hom_ext — Mathlib

English

If F1 and F2 agree on each of the generators of Free_R X, then F1 = F2.

Русский

Если F1 и F2 совпадают на каждом генераторе Free_R X, то F1 = F2.

LaTeX

$$$ \forall x, F_1(\operatorname{of}_R x) = F_2(\operatorname{of}_R x) \;\Rightarrow\; F_1 = F_2. $$$

Lean4

@[ext]
theorem hom_ext {F₁ F₂ : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A} (h : ∀ x, F₁ (of R x) = F₂ (of R x)) : F₁ = F₂ :=
  (lift R).symm.injective <| funext h

Похожие утверждения