toPadicInt — Mathlib

English

The cardinality of TruncatedWittVector p n (ZMod p) equals p^n.

Русский

Кардиналность TruncatedWittVector p n (ZMod p) равна p^n.

LaTeX

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

Lean4

/-- `toPadicInt` lifts `toZModPow : 𝕎 (ZMod p) →+* ZMod (p ^ k)` to a ring hom to `ℤ_[p]`
using `PadicInt.lift`, the universal property of `ℤ_[p]`.
-/
def toPadicInt : 𝕎 (ZMod p) →+* ℤ_[p] :=
  PadicInt.lift <| toZModPow_compat p

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