zmodEquivTrunc — Mathlib

English

There is a unique ring isomorphism between ZMod(p^n) and TruncatedWittVector p n (ZMod p).

Русский

Существует единственный кольцевой изоморфизм между ZMod(p^n) и TruncatedWittVector p n (ZMod p).

LaTeX

$$$$ ZMod(p^n) \cong^+_\* \mathrm{TruncatedWittVector}_p^n (\mathbb{Z}/p\mathbb{Z}). $$$$

Lean4

/-- 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`.
-/
def zmodEquivTrunc : ZMod (p ^ n) ≃+* TruncatedWittVector p n (ZMod p) :=
  ZMod.ringEquiv (TruncatedWittVector p n (ZMod p)) (card_zmod _ _)

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