hom_ext — Mathlib

English

Two ring homomorphisms from FreeCommRing α to R are equal if they agree on the generators of α.

Русский

Два кольцевых гомоморфизма от FreeCommRing α в R равны, если они согласуются на генераторах α.

LaTeX

$$$ \\forall f,g : \\mathrm{FreeCommRing}(\\alpha) \\to\\!+* R,\\ (\\forall x, f(\\mathrm{of}(x)) = g(\\mathrm{of}(x))) \\Rightarrow f = g $$$

Lean4

@[ext 1100]
theorem hom_ext ⦃f g : FreeCommRing α →+* R⦄ (h : ∀ x, f (of x) = g (of x)) : f = g :=
  lift.symm.injective (funext h)

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