ringHom_eq_of_ker_eq — Mathlib

English

Two ring homomorphisms R → ZMod n with equal kernels are equal.

Русский

Два кольцевых гомоморфизма R → ZMod n с равными ядрами совпадают.

LaTeX

$$$\\\\forall f,g: R \\rightarrow ZMod(n), \\\\ ker f = ker g \\Rightarrow f = g.$$$

Lean4

/-- Two ring homomorphisms into `ZMod n` with equal kernels are equal. -/
theorem ringHom_eq_of_ker_eq {n : ℕ} {R : Type*} [Ring R] (f g : R →+* ZMod n) (h : RingHom.ker f = RingHom.ker g) :
    f = g := by
  have := f.liftOfRightInverse_comp _ (ZMod.ringHom_rightInverse f) ⟨g, le_of_eq h⟩
  rw [Subtype.coe_mk] at this
  rw [← this, RingHom.ext_zmod (f.liftOfRightInverse _ _ ⟨g, _⟩) _, RingHom.id_comp]

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