commutes' — Mathlib

English

The pointwise version of the commutativity holds: for all i appropriate, truncation of the zmodEquivTrunc image equals the zmodEquivTrunc of the cast image.

Русский

Точечная версия коммутативности: для всех подходящих i при применении усечения и отображения сохраняются равенства.

LaTeX

$$$$ \forall x:\, ZMod(p^m),\; \text{truncate}(hm)( zmodEquivTrunc\ p\ m\ x ) = zmodEquivTrunc\ p\ n ( ZMod.castHom (pow\_dvd\_pow p hm) _ (x) ). $$$$

Lean4

theorem commutes' {m : ℕ} (hm : n ≤ m) (x : ZMod (p ^ m)) :
    truncate hm (zmodEquivTrunc p m x) = zmodEquivTrunc p n (ZMod.castHom (pow_dvd_pow p hm) _ x) :=
  show (truncate hm).comp (zmodEquivTrunc p m).toRingHom x = _ by rw [commutes _ _ hm]; rfl

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