English
The function wittMulN(p,n) encodes how the Witt vector x multiplies by the natural number n, expressed as a family of multivariate polynomials with integer coefficients.
Русский
Функция wittMulN(p,n) кодирует умножение Witt-вектора на число n, выраженное через множество полиномов с целочисленными коэффициентами.
LaTeX
$$$wittMulN: \mathbb{N} \to \mathbb{N} \to \mathrm{MvPolynomial}_{\mathbb{N}, \mathbb{Z}}$ with recursive definition $wittMulN\;0 = 0$, $wittMulN\; (n+1) = \text{bind}_1 (\lambda k, ![wittMulN\;n, X]) (wittAdd\ p\ k)$$$
Lean4
/-- `wittMulN p n` is the family of polynomials that computes
the coefficients of `x * n` in terms of the coefficients of the Witt vector `x`. -/
noncomputable def wittMulN : ℕ → ℕ → MvPolynomial ℕ ℤ
| 0 => 0
| n + 1 => fun k => bind₁ (Function.uncurry <| ![wittMulN n, X]) (wittAdd p k)
