pow_dvd_nthHom_sub — Mathlib

English

For i ≤ j, p^i divides nthHom f r j − nthHom f r i.

Русский

Для i ≤ j, p^i делит nthHom f r j − nthHom f r i.

LaTeX

$$(p : ℤ)^i ∣ (nthHom f r j) − (nthHom f r i)$$

Lean4

theorem pow_dvd_nthHom_sub (r : R) (i j : ℕ) (h : i ≤ j) : (p : ℤ) ^ i ∣ nthHom f r j - nthHom f r i :=
  by
  specialize f_compat i j h
  rw [← Int.natCast_pow, ← ZMod.intCast_zmod_eq_zero_iff_dvd, Int.cast_sub]
  dsimp [nthHom]
  rw [← f_compat, RingHom.comp_apply]
  simp only [ZMod.cast_id, ZMod.castHom_apply, sub_self, ZMod.natCast_val, ZMod.intCast_cast]

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