Theorems · Definition · number theory

TruncatedWittVector.zmodEquivTrunc

(p : ℕ) → [hp : Fact (Nat.Prime p)] → (n : ℕ) → ZMod (p ^ n) ≃+* TruncatedWittVector p n (ZMod p)

The unique isomorphism between ZMod p^n and TruncatedWittVector p n (ZMod p). This isomorphism exists, because TruncatedWittVector p n (ZMod p) is a finite ring with characteristic and cardinality p^n.

Defined in

Mathlib.RingTheory.WittVector.Compare

Cited by

9 results in Mathlib

Foundations

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

Assumes

Fact