ringHom_ext — Mathlib

English

If j and k are ring homomorphisms S → P and j ∘ algebraMap_R_S = k ∘ algebraMap_R_S, then j = k.

Русский

Если j и k — кольсовые гомоморфизмы S → P и они совпадают на образе R в S, тогда j = k.

LaTeX

$$$ \\forall j,k : S \\to P,\\; j \\circ (\\mathrm{algebraMap}_{R,S}) = k \\circ (\\mathrm{algebraMap}_{R,S}) \\Rightarrow j = k. $$$

Lean4

/-- See note [partially-applied ext lemmas] -/
theorem ringHom_ext {P : Type*} [Semiring P] ⦃j k : S →+* P⦄ (h : j.comp (algebraMap R S) = k.comp (algebraMap R S)) :
    j = k :=
  RingHom.coe_monoidHom_injective <| monoidHom_ext M <| MonoidHom.ext <| RingHom.congr_fun h

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