toIntAlgHom_injective — Mathlib

English

The map sending a ring hom to its integer-algebra lift is injective: if f.toIntAlgHom = g.toIntAlgHom, then f = g.

Русский

Отображение кольцевого гомоморфизма в соответствующий интеґральный алгебраический гомоморфизм инъективно: если f.toIntAlgHom = g.toIntAlgHom, то f = g.

LaTeX

$$$ (f^{\\mathrm{IntAlg}} = g^{\\mathrm{IntAlg}}) \\Rightarrow (f = g) $$$

Lean4

theorem toIntAlgHom_injective [Ring R] [Ring S] : Function.Injective (RingHom.toIntAlgHom : (R →+* S) → _) :=
  fun _ _ e ↦ DFunLike.ext _ _ (fun x ↦ DFunLike.congr_fun e x)

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