English
A precise expression for polyOfInterest in terms of its factors shows how the variable set is composed with the Witt components after renaming. This is a refinement of the previous var equality.
Русский
Точная формула polyOfInterest через его множители демонстрирует состав множества переменных после переименования Witt-компонентов. Это уточнение предыдущего равенства переменных.
LaTeX
$$$(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)) (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 (n : ℕ) : (polyOfInterest p n).vars ⊆ univ ×ˢ range (n + 1) := by
rw [polyOfInterest_vars_eq]; apply mul_polyOfInterest_vars
