zmod_cast_comp_toZModPow — Mathlib

English

Nat.cast has dense range in ℤ_p.

Русский

Образ Nat.cast в ℤ_p плотен.

LaTeX

$$DenseRange Nat.cast$$

Lean4

theorem zmod_cast_comp_toZModPow (m n : ℕ) (h : m ≤ n) :
    (ZMod.castHom (pow_dvd_pow p h) (ZMod (p ^ m))).comp (@toZModPow p _ n) = @toZModPow p _ m :=
  by
  apply ZMod.ringHom_eq_of_ker_eq
  ext x
  rw [RingHom.mem_ker, RingHom.mem_ker]
  simp only [Function.comp_apply, ZMod.castHom_apply, RingHom.coe_comp]
  simp only [toZModPow, toZModHom, RingHom.coe_mk]
  dsimp
  rw [ZMod.cast_natCast (pow_dvd_pow p h), zmod_congr_of_sub_mem_span m (x.appr n) (x.appr n) (x.appr m)]
  · rw [sub_self]
    apply Ideal.zero_mem _
  · rw [Ideal.mem_span_singleton]
    rcases dvd_appr_sub_appr x m n h with ⟨c, hc⟩
    use c
    rw [← Nat.cast_sub (appr_mono _ h), hc, Nat.cast_mul, Nat.cast_pow]

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