English
If i ≤ n and (p : TruncatedWittVector p n R)^i = 0, then i = n, under CharP p
Русский
Если i ≤ n и (p): TruncatedWittVector p n R)^i = 0, тогда i = n при CharP
LaTeX
$$$$ \forall i \le n,\; (p : \mathrm{TruncatedWittVector}_p^n R)^i = 0 \Rightarrow i = n. $$$$
Lean4
theorem toZModPow_compat (m n : ℕ) (h : m ≤ n) :
(ZMod.castHom (pow_dvd_pow p h) (ZMod (p ^ m))).comp (toZModPow p n) = toZModPow p m :=
calc
(ZMod.castHom _ (ZMod (p ^ m))).comp ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate n))
_ = ((zmodEquivTrunc p m).symm.toRingHom.comp (TruncatedWittVector.truncate h)).comp (truncate n) := by
rw [commutes_symm, RingHom.comp_assoc]
_ = (zmodEquivTrunc p m).symm.toRingHom.comp (truncate m) := by
rw [RingHom.comp_assoc, truncate_comp_wittVector_truncate]
