English
If two multiplicative monoid homomorphisms f,g from FreeMagma α to β agree on the inclusion map of α (i.e., f ∘ of = g ∘ of), then f = g.
Русский
Если два гомоморфизма свободной магмы α в β совпадают на инклюзии α в FreeMagma α (то есть f ∘ of = g ∘ of), то они равны.
LaTeX
$$$$\text{If } f,g: FreeMagma(\alpha) \to_{*} \beta \text{ satisfy } f \circ of = g \circ of, \text{ then } f = g. $$$$
Lean4
@[to_additive (attr := ext 1100)]
theorem hom_ext {β : Type v} [Mul β] {f g : FreeMagma α →ₙ* β} (h : f ∘ of = g ∘ of) : f = g :=
(DFunLike.ext _ _) fun x ↦ recOnMul x (congr_fun h) <| by intros; simp only [map_mul, *]
