zmodEquivTrunc_compat — Mathlib

English

Compatibility of truncation with ZMod cast via PadicInt

Русский

Совместимость усечения с ZMod через PadicInt

LaTeX

$$$$ (TruncatedWittVector.truncate hk).\comp ((TruncatedWittVector.zmodEquivTrunc p k_2).toRingHom.comp (PadicInt.toZModPow k_2)) = (TruncatedWittVector.zmodEquivTrunc p k_1).toRingHom.comp (PadicInt.toZModPow k_1). $$$$

Lean4

theorem zmodEquivTrunc_compat (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂) :
    (TruncatedWittVector.truncate hk).comp ((zmodEquivTrunc p k₂).toRingHom.comp (PadicInt.toZModPow k₂)) =
      (zmodEquivTrunc p k₁).toRingHom.comp (PadicInt.toZModPow k₁) :=
  by rw [← RingHom.comp_assoc, commutes, RingHom.comp_assoc, PadicInt.zmod_cast_comp_toZModPow _ _ hk]

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