Update S01_Calculating.lean

Fix typo
avigad · Feb 5, 2024 · 144e0b8 · 144e0b8
1 parent 3862e04
commit 144e0b8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/MIL/C02_Basics/S01_Calculating.lean b/MIL/C02_Basics/S01_Calculating.lean
@@ -163,7 +163,7 @@ example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
   rw [mul_assoc]
 
 /- TEXT:
-You an also use ``rw`` with facts from the local context.
+You can also use ``rw`` with facts from the local context.
 TEXT. -/
 -- Using facts from the local context.
 -- QUOTE: