English
The ring of Witt vectors over ZMod p is isomorphic to the ring of p-adic integers; witness by toPadicInt with inverse fromPadicInt.
Русский
Кольцо Witt над ZMod p изоморфно кольцу p-адических целых; доказательство через toPadicInt и fromPadicInt.
LaTeX
$$$$ \mathbb{W}_p(\mathbb{Z}/p\mathbb{Z}) \cong^+_* \mathbb{Z}_{(p)}. $$$$
Lean4
/-- The ring of Witt vectors over `ZMod p` is isomorphic to the ring of `p`-adic integers. This
equivalence is witnessed by `WittVector.toPadicInt` with inverse `WittVector.fromPadicInt`.
-/
def equiv : 𝕎 (ZMod p) ≃+* ℤ_[p] where
toFun := toPadicInt p
invFun := fromPadicInt p
left_inv := fromPadicInt_comp_toPadicInt_ext _
right_inv := toPadicInt_comp_fromPadicInt_ext _
map_mul' := RingHom.map_mul _
map_add' := RingHom.map_add _
