fix missing by (#126)

avigad · Sep 10, 2023 · 9fbe1f9 · 9fbe1f9
1 parent df6a935
commit 9fbe1f9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean b/MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
@@ -404,7 +404,7 @@ theorem one_add_one_eq_two : 1 + 1 = (2 : R) := by
   norm_num
 
 -- EXAMPLES:
-theorem two_mul (a : R) : 2 * a = a + a :=
+theorem two_mul (a : R) : 2 * a = a + a := by
   sorry
 -- QUOTE.