hom_ext — Mathlib

English

Two ring homomorphisms f,g: FreeRing α →+* R are equal if they agree on all generators of α: f(of x) = g(of x) for all x ∈ α.

Русский

Две кольцевые гомоморфизма f,g: FreeRing α →+* R равны, если они совпадают на всех порождающих α: f(of x) = g(of x) для всех x из α.

LaTeX

$$$$ \forall f,g: FreeRing(\alpha) \to_+* R,\ (\forall x:\alpha,\ f(\mathrm{of}(x)) = g(\mathrm{of}(x))) \Rightarrow f = g. $$$$

Lean4

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

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