ker_toZModPow — Mathlib

English

The kernel of toZModPow(n) is the ideal generated by p^n.

Русский

Ядро toZModPow(n) равно идеалу, порождённому p^n.

LaTeX

$$RingHom.ker (toZModPow n) = Ideal.span { (p^n) }$$

Lean4

theorem ker_toZModPow (n : ℕ) : RingHom.ker (toZModPow n : ℤ_[p] →+* ZMod (p ^ n)) = Ideal.span {(p : ℤ_[p]) ^ n} :=
  by
  ext x
  rw [RingHom.mem_ker]
  constructor
  · intro h
    suffices x.appr n = 0 by
      convert appr_spec n x
      simp only [this, sub_zero, cast_zero]
    dsimp [toZModPow, toZModHom] at h
    rw [ZMod.natCast_eq_zero_iff] at h
    apply eq_zero_of_dvd_of_lt h (appr_lt _ _)
  · intro h
    rw [← sub_zero x] at h
    dsimp [toZModPow, toZModHom]
    rw [zmod_congr_of_sub_mem_span n x _ 0 _ h, cast_zero]
    apply appr_spec

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