English
Two monoid homomorphisms f,g: G/N →* M are equal if they agree after composing with mk' N.
Русский
Два моноид-хомоморфизма f,g: G/N →* M равны, если их композиции с mk' N совпадают.
LaTeX
$$If $f,g: G/N \\to M$ satisfy $f \\circ (mk' N) = g \\circ (mk' N)$, then $f = g$.$$
Lean4
/-- Two `MonoidHom`s from a quotient group are equal if their compositions with
`QuotientGroup.mk'` are equal.
See note [partially-applied ext lemmas]. -/
@[to_additive (attr := ext 1100) /-- Two `AddMonoidHom`s from an additive quotient group are equal
if their compositions with `AddQuotientGroup.mk'` are equal.
See note [partially-applied ext lemmas]. -/
]
theorem monoidHom_ext ⦃f g : G ⧸ N →* M⦄ (h : f.comp (mk' N) = g.comp (mk' N)) : f = g :=
MonoidHom.ext fun x => QuotientGroup.induction_on x <| (DFunLike.congr_fun h :)
