Theorems · Definition · commutative algebra

wittPolynomial

ℕ → (R : Type u_1) → [inst : CommRing R] → ℕ → MvPolynomial ℕ R

wittPolynomial p R n is the n-th Witt polynomial with respect to a prime p with coefficients in a commutative ring R. It is defined as: ∑_{i ≤ n} p^i X_i^{p^{n-i}} ∈ R[X_0, X_1, X_2, …].

Defined in

Mathlib.RingTheory.WittVector.WittPolynomial

Cited by

54 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing