We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent cdba786 commit 13808e5Copy full SHA for 13808e5
1 file changed
Mathlib/GroupTheory/Congruence/Hom.lean
@@ -40,7 +40,6 @@ namespace Con
40
section Mul
41
variable {F} [Mul M] [Mul N] [Mul P] [FunLike F M N] [MulHomClass F M N]
42
43
-
44
/-- The natural homomorphism from a magma to its quotient by a congruence relation. -/
45
@[to_additive (attr := simps) /-- The natural homomorphism from an additive magma to its quotient by
46
an additive congruence relation. -/]
0 commit comments