ker_toZMod — Mathlib

English

The kernel of the map to ZMod p is the maximal ideal of ℤ_p.

Русский

Ядро отображения к ZMod p совпадает с максимальным идеалом ℤ_p.

LaTeX

$$Ker(toZMod) = maximalIdeal(ℤ_[p])$$

Lean4

theorem ker_toZMod : RingHom.ker (toZMod : ℤ_[p] →+* ZMod p) = maximalIdeal ℤ_[p] :=
  by
  ext x
  rw [RingHom.mem_ker]
  constructor
  · intro h
    simpa only [h, ZMod.cast_zero, sub_zero] using toZMod_spec x
  · intro h
    rw [← sub_zero x] at h
    dsimp [toZMod, toZModHom]
    convert zmod_congr_of_sub_mem_max_ideal x _ 0 _ h
    · norm_cast
    · apply sub_zmodRepr_mem

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