English
Let x and y be Witt vectors over a commutative ring R. Then for every natural number n, the n-th coefficient of the product x · y is obtained by evaluating the Witt polynomial wittMul at the pair of coefficient sequences [x.coeff, y.coeff].
Русский
Пусть x и y — витытые векторы над симметричным кольцом R. Тогда для любого натурального числа n n-й коэффициент произведения x · y равен значениям полинома Витта wittMul, применённого к паре последовательностей коэффициентов [x.coeff, y.coeff].
LaTeX
$$$(x \cdot y).\text{coeff } n = \operatorname{peval}(\operatorname{wittMul}(p,n), [x.coeff, y.coeff])$$$
Lean4
theorem mul_coeff (x y : 𝕎 R) (n : ℕ) : (x * y).coeff n = peval (wittMul p n) ![x.coeff, y.coeff] := by
simp [(· * ·), Mul.mul, eval]
