diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean index dd35253..8f3c65c 100644 --- a/CommAlg/final_poly_type.lean +++ b/CommAlg/final_poly_type.lean @@ -26,7 +26,7 @@ macro "obviously" : tactic => -- Testing of Polynomial section Polynomial noncomputable section - + example (f : Polynomial ℚ) (hf : f = Polynomial.C (1 : ℚ)) : Polynomial.eval 2 f = 1 := by have : ∀ (q : ℚ), Polynomial.eval q f = 1 := by sorry