誤字を修正

lean-ja · Sep 22, 2023 · 107a3a7 · 107a3a7
1 parent 85226e2
commit 107a3a7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Examples/ApplyQuestion.lean b/Examples/ApplyQuestion.lean
@@ -5,7 +5,7 @@ import Mathlib.Algebra.Hom.Group.Defs
 
 
 -- ANCHOR: first
--- 群順同型は積を保つ
+-- 群準同型は積を保つ
 example [Group G] [Group H] (f : G →* H) (a b : G) :
     f (a * b) = f a * f b := by
     -- `exact MonoidHom.map_mul f a b` を提案してくれる