English
The n-th Witt polynomial with respect to a prime p and coefficient ring R is the sum over i = 0..n of p^i times X_i^{p^{n−i}}; equivalently, ∑_{i=0}^{n} p^i X_i^{p^{n−i}}.
Русский
Н-ая полином Витта относительно простого p и кольца R задаётся как сумма по i=0..n от p^i X_i^{p^{n−i}}.
LaTeX
$$$$ wittPolynomial(p,R,n) = \\sum_{i=0}^{n} p^i \\; X_i^{p^{\,n-i}}. $$$$
Lean4
/-- `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, …]`. -/
noncomputable def wittPolynomial (n : ℕ) : MvPolynomial ℕ R :=
∑ i ∈ range (n + 1), monomial (single i (p ^ (n - i))) ((p : R) ^ i)
