ker_intCastRingHom — Mathlib

English

The kernel of the natural ring homomorphism Int.castRingHom: Z → ZMod n is exactly the ideal generated by n.

Русский

Явный ядро естественного кольцевого гомоморфа Int.castRingHom: Z → ZMod n равно идеалу, порождённому n.

LaTeX

$$$\\\\ker(\\\\text{Int.castRingHom}\\\\ (ZMod n)) = \\\\langle n \\\\rangle \\\\subseteq \\\\mathbb{Z}.$$$

Lean4

/-- The ring homomorphism `ℤ → ZMod n` has kernel generated by `n`. -/
theorem ker_intCastRingHom (n : ℕ) : RingHom.ker (Int.castRingHom (ZMod n)) = Ideal.span ({(n : ℤ)} : Set ℤ) :=
  by
  ext
  rw [Ideal.mem_span_singleton, RingHom.mem_ker, Int.coe_castRingHom, ZMod.intCast_zmod_eq_zero_iff_dvd]

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