fix spaces in 'Rational' example #48

leanprover-community · Jan 13, 2025 · c231a9f · c231a9f
1 parent 13c6e55
commit c231a9f
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Projects/mathlib-demo/MathlibLatest/Rational.lean b/Projects/mathlib-demo/MathlibLatest/Rational.lean
@@ -9,7 +9,7 @@ variable (x y z : ℚ)
 example (h₁ : x < y) (h₂ : y + 3 < z + 10) : x + 37 < z + 44 := by
   linarith -- the `linarith` tactic can do this automatically
 
--- let's prove that (x+y)^2=x^2+2*x*y+y^2
+-- let's prove that (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2
 
-example : (x + y)^2 = x^2 + 2 * x * y + y^2 := by
+example : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
   ring -- the `ring` tactic can do this automatically