English
The full set of variables of polyOfInterest equals the scaled Witt convolution expression, which is itself built from wittMul and X-variables with renamed Witt polynomials. It clarifies the precise variable structure of polyOfInterest.
Русский
Полный набор переменных polyOfInterest совпадает с выражением, полученным путем умножения Witt инициализаций и переименованных Witt-полиномов. Это уточняет точную структуру переменных polyOfInterest.
LaTeX
$$$(polyOfInterest\ p\ n).vars = ((p^{n+1}) \cdot (wittMul\ p\ (n+1) + (p^{n+1}) X(0,n+1) X(1,n+1) - X(0,n+1) rename(Prod.mk(1)) (wittPolynomial p\; \mathbb{Z})(n+1) - X(1,n+1) rename(Prod.mk(0)) (wittPolynomial p\; \mathbb{Z})(n+1))).vars$$$
Lean4
theorem polyOfInterest_vars_eq (n : ℕ) :
(polyOfInterest p n).vars =
((p : 𝕄) ^ (n + 1) *
(wittMul p (n + 1) + (p : 𝕄) ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
X (0, n + 1) * rename (Prod.mk (1 : Fin 2)) (wittPolynomial p ℤ (n + 1)) -
X (1, n + 1) * rename (Prod.mk (0 : Fin 2)) (wittPolynomial p ℤ (n + 1)))).vars :=
by
have : (p : 𝕄) ^ (n + 1) = C ((p : ℤ) ^ (n + 1)) := by norm_cast
rw [polyOfInterest, this, vars_C_mul]
apply pow_ne_zero
exact mod_cast hp.out.ne_zero
