card — Mathlib

English

If R is finite, then the cardinality of the truncated Witt vectors is card(R)^n.

Русский

Если R конечно, то кардиналность усечённых виттовых векторов равна |R|^n.

LaTeX

$$$$\\#\\mathrm{TruncatedWittVector}_p^n R = (\\#R)^n. $$$$

Lean4

theorem card {R : Type*} [Fintype R] : Fintype.card (TruncatedWittVector p n R) = Fintype.card R ^ n := by
  simp only [TruncatedWittVector, Fintype.card_fin, Fintype.card_fun]

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