English
A homomorphisms from the free monoid are determined by their values on generators: if two monoid homomorphisms f and g agree on of x for all x, then f = g.
Русский
Гомоморфизмы из свободного моноида определяются по значениям на образах генераторов: если f и g согласны на of x для всех x, то f = g.
LaTeX
$$$\\\\forall f,g : FreeMonoid α \\to^* M, \\\\; (\\\\forall x, f(\\\\operatorname{of} x) = g(\\\\operatorname{of} x)) \\\\Rightarrow f = g$$$
Lean4
@[to_additive (attr := ext)]
theorem hom_eq ⦃f g : FreeMonoid α →* M⦄ (h : ∀ x, f (of x) = g (of x)) : f = g :=
MonoidHom.ext fun l ↦
recOn l (f.map_one.trans g.map_one.symm) (fun x xs hxs ↦ by simp only [h, hxs, MonoidHom.map_mul])
