Update src/Init/Core.lean

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
leanprover · Jan 22, 2024 · ad84c63 · ad84c63
1 parent b27bc26
commit ad84c63
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
@@ -1762,7 +1762,7 @@ proof.
 
 This class is intended for simplifying defining instances of
 `LawfulIdentity` and functions needed commutative operations with
-identity should just add a `LawfulIdentity constraint.
+identity should just add a `LawfulIdentity` constraint.
 -/
 class LawfulCommIdentity (op : α → α → α) (o : outParam α) [hc : Commutative op] extends LawfulIdentity op o : Prop where
   left_id a := Eq.trans (hc.comm o a) (right_id a)