commutes_symm' — Mathlib

English

Symmetric version of the commutativity: the symmetric diagram commutes with the reversed roles of the maps.

Русский

Симметричная версия коммутативности: диаграмма симметрична по ролям стрелок и также commute.

LaTeX

$$$$ (zmodEquivTrunc\ p\ n).symm.toRingHom \circ (truncate hm) = (ZMod.castHom (pow\_dvd\_pow p hm) _).\circ (zmodEquivTrunc\ p\ m).symm.toRingHom. $$$$

Lean4

theorem commutes_symm' {m : ℕ} (hm : n ≤ m) (x : TruncatedWittVector p m (ZMod p)) :
    (zmodEquivTrunc p n).symm (truncate hm x) = ZMod.castHom (pow_dvd_pow p hm) _ ((zmodEquivTrunc p m).symm x) :=
  by
  apply (zmodEquivTrunc p n).injective
  rw [← commutes' _ _ hm]
  simp

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