From 404943e45e5fba5489e1220aa230d1ed30bfc5c9 Mon Sep 17 00:00:00 2001 From: Andre Date: Fri, 16 Jun 2023 19:15:46 -0400 Subject: [PATCH] white space --- CommAlg/final_poly_type.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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