Theorems · Theorem · number theory

TruncatedWittVector.commutes_symm

∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) {m : ℕ} (hm : n ≤ m),
  (TruncatedWittVector.zmodEquivTrunc p n).symm.toRingHom.comp (TruncatedWittVector.truncate hm) =
    (ZMod.castHom ⋯ (ZMod (p ^ n))).comp (TruncatedWittVector.zmodEquivTrunc p m).symm.toRingHom

The following diagram commutes: ``text TruncatedWittVector p n (ZMod p) -> TruncatedWittVector p m (ZMod p) | | | | v v ZMod (p^n) -> ZMod (p^m) ` Here the vertical arrows are (TruncatedWittVector.zmodEquivTrunc p _).symm, the horizontal arrow at the top is ZMod.castHom, and the horizontal arrow at the bottom is TruncatedWittVector.truncate`.

Defined in

Mathlib.RingTheory.WittVector.Compare

Cited by

1 results in Mathlib

Foundations

Depth 151 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fact