English
Let f,g be semigroup homomorphisms from FreeSemigroup α to β. If f and g agree on the generators, i.e. f ∘ of = g ∘ of, then f = g. Thus a homomorphism from FreeSemigroup α is determined by its values on α.
Русский
Пусть f, g — гомоморфизмы полугрупп FreeSemigroup α → β. Если они согласованы на генераторах, то f = g; следовательно гомоморфизм определяется значениями на α.
LaTeX
$$If f,g : FreeSemigroup α →⋅ β satisfy f ∘ of = g ∘ of, then f = g.$$
Lean4
@[to_additive (attr := ext 1100)]
theorem hom_ext {β : Type v} [Mul β] {f g : FreeSemigroup α →ₙ* β} (h : f ∘ of = g ∘ of) : f = g :=
(DFunLike.ext _ _) fun x ↦ FreeSemigroup.recOnMul x (congr_fun h) fun x y hx hy ↦ by simp only [map_mul, *]
