Leading terms of Witt vector multiplication #
The goal of this file is to study the leading terms of the formula for the
of a product of Witt vectors
y over a ring of characteristic
We aim to isolate the
n+1st coefficients of
y, and express the rest of the product
in terms of a function of the lower coefficients.
For most of this file we work with terms of type
MvPolynomial (Fin 2 × ℕ) ℤ.
We will eventually evaluate them in
k, but first we must take care of a calculation
that needs to happen in characteristic 0.
Main declarations #
WittVector.nth_mul_coeff: expresses the coefficient of a product of Witt vectors in terms of the previous coefficients of the multiplicands.
p version of