Theorems · Inductive type · commutative algebra

WittVector

ℕ → Type u_1 → Type u_1

WittVector p R is the ring of p-typical Witt vectors over the commutative ring R, where p is a prime number. If p is invertible in R, this ring is isomorphic to ℕ → R (the product of ℕ copies of R). If R is a ring of characteristic p, then WittVector p R is a ring of characteristic 0. The canonical example is WittVector p (ZMod p), which is isomorphic to the p-adic integers ℤ_[p].

Defined in

Mathlib.RingTheory.WittVector.Defs

Cited by

227 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms