Add a missing by in an exercise.

Fixes #125
avigad · Sep 10, 2023 · df6a935 · df6a935
1 parent 02c54eb
commit df6a935
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
@@ -379,7 +379,7 @@ variable {R : Type*} [Ring R]
 
 -- EXAMPLES:
 -- QUOTE:
-theorem self_sub (a : R) : a - a = 0 :=
+theorem self_sub (a : R) : a - a = 0 := by
   sorry
 -- QUOTE.