card_zmod

Mathlib.RingTheory.WittVector.Compare

URI: https://scilib.ai/kg/mathlib#TruncatedWittVector.card_zmod

English

The cardinality of the truncated Witt vectors over ZMod p is p^n.

Русский

Кардиналность усечённых Witt-векторов над ZMod p равна p^n.

LaTeX

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

Lean4

theorem card_zmod : Fintype.card (TruncatedWittVector p n (ZMod p)) = p ^ n := by rw [card, ZMod.card]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru