English
For a prime p and an integer vector y, define the Witt polynomial product at n by taking two copies of the Witt polynomial and renaming their coordinates 0 and 1, then multiplying them.
Русский
Для простого числа p и вектора y целых чисел определим произведение полиномов Витта в позиции n как произведение двух копий полинома Витта после переименования координат 0 и 1.
LaTeX
$$$ \mathrm{wittPolyProd}(n) = \mathrm{rename}(\mathrm{Prod.mk}(0, \!\text{Fin } 2))(\mathrm{wittPolynomial}(p, \mathbb{Z}, n)) \cdot \mathrm{rename}(\mathrm{Prod.mk}(1, \!\text{Fin } 2))(\mathrm{wittPolynomial}(p, \mathbb{Z}, n)) $$$
Lean4
/-- ```
(∑ i ∈ range n, (y.coeff i)^(p^(n-i)) * p^i.val) *
(∑ i ∈ range n, (y.coeff i)^(p^(n-i)) * p^i.val)
```
-/
def wittPolyProd (n : ℕ) : 𝕄 :=
rename (Prod.mk (0 : Fin 2)) (wittPolynomial p ℤ n) * rename (Prod.mk (1 : Fin 2)) (wittPolynomial p ℤ n)
