toZModPow — Mathlib

English

For any prime p and R nontrivial, the Witt vector ring 𝕎_p(R) is nontrivial.

Русский

Для любого простого p и ненулевого R кольцо Witt 𝕎_p(R) ненулево.

LaTeX

$$$$ \mathbb{W}_p(R) \neq \{0\}. $$$$

Lean4

/-- `toZModPow` is a family of compatible ring homs. We get this family by composing
`TruncatedWittVector.zmodEquivTrunc` (in right-to-left direction) with `WittVector.truncate`. -/
def toZModPow (k : ℕ) : 𝕎 (ZMod p) →+* ZMod (p ^ k) :=
  (zmodEquivTrunc p k).symm.toRingHom.comp (truncate k)

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