typo in L06mul_right_eq_one.lean

leanprover-community · Jun 14, 2024 · 5d25d0f · 5d25d0f
1 parent 9bc5995
commit 5d25d0f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean b/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean
@@ -38,7 +38,7 @@ to the context, because you just supplied the proof of it (`succ_inj a b`).
 ## Example
 
 If you have a proof to hand, then you don't even need to state what you
-are proving. example
+are proving. For example
 
 `have h2 := succ_inj a b`