charP_zmod — Mathlib

English

The truncated Witt vectors have characteristic p^n when built over ZMod p.

Русский

Утверждается, что характеристика усечённых Witt-векторов над ZMod p равна p^n.

LaTeX

$$$$ \operatorname{Char}( \mathrm{TruncatedWittVector}_p^n(\mathbb{Z}/p\mathbb{Z}) ) = p^n. $$$$

Lean4

theorem charP_zmod : CharP (TruncatedWittVector p n (ZMod p)) (p ^ n) :=
  charP_of_prime_pow_injective _ _ _ (card_zmod _ _) (eq_of_le_of_cast_pow_eq_zero p n (ZMod p))

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