English
If two monoid homomorphisms from the presented monoid to M agree on all images of generators, they are equal.
Русский
Если два моноидных гомоморфизма от представленного моноида в M совпадают на изображениях всех генераторов, они равны.
LaTeX
$$$\forall \phi, \psi: \operatorname{PresentedMonoid rels} \to^* M,\ \forall a:\alpha, \phi(\operatorname{of rels} a) = \psi(\operatorname{of rels} a) \Rightarrow \phi = \psi$$$
Lean4
@[to_additive (attr := ext)]
theorem ext {M : Type*} [Monoid M] (rels : FreeMonoid α → FreeMonoid α → Prop) {φ ψ : PresentedMonoid rels →* M}
(hx : ∀ (x : α), φ (.of rels x) = ψ (.of rels x)) : φ = ψ :=
by
apply MonoidHom.eq_of_eqOn_denseM (closure_range_of _)
grind [Set.eqOn_range]
