English
The remainder term depends only on the first n Witt coordinates; its variable set is contained in the first n+1 coordinates.
Русский
Остаток зависит только от первых n координат Witt и его переменные ограничены первыми n+1 координатами.
LaTeX
$$$\text{remainder}(p,n).vars \subseteq \text{univ} \times\text{range}(n+1).$$$
Lean4
theorem remainder_vars (n : ℕ) : (remainder p n).vars ⊆ univ ×ˢ range (n + 1) :=
by
rw [remainder]
apply Subset.trans (vars_mul _ _)
refine union_subset ?_ ?_ <;>
· refine Subset.trans (vars_sum_subset _ _) ?_
rw [biUnion_subset]
intro x hx
rw [rename_monomial, vars_monomial, Finsupp.mapDomain_single]
· apply Subset.trans Finsupp.support_single_subset
simpa using mem_range.mp hx
· apply pow_ne_zero
exact mod_cast hp.out.ne_zero
