English
For a Witt polynomial wittPolynomial p R n over a ring R with CharZero, the set of variables appearing is exactly {0,1,...,n}.
Русский
Для полинома Витта wittPolynomial p R n над кольцом R с CharZero множества переменных равны {0,1,...,n}.
LaTeX
$$(wittPolynomial p R n).vars = range (n + 1)$$
Lean4
theorem wittPolynomial_vars [CharZero R] (n : ℕ) : (wittPolynomial p R n).vars = range (n + 1) :=
by
have : ∀ i, (monomial (Finsupp.single i (p ^ (n - i))) ((p : R) ^ i)).vars = { i } :=
by
intro i
refine vars_monomial_single i (pow_ne_zero _ hp.1) ?_
rw [← Nat.cast_pow, Nat.cast_ne_zero]
exact pow_ne_zero i hp.1
rw [wittPolynomial, vars_sum_of_disjoint]
· simp only [this, biUnion_singleton_eq_self]
· simp only [this]
intro a b h
apply disjoint_singleton_left.mpr
rwa [mem_singleton]
