English
For a nonzero coefficient r, the variables of monomial(s) with that coefficient equal the support of s.
Русский
Для ненулевого коэффициента r переменные монома monomial(s) совпадают с опорой s.
LaTeX
$$$$ \mathrm{vars}(\mathrm{monomial}(s)) = \mathrm{support}(s) $$$$
Lean4
/-- The variables of the product of a family of polynomials
are a subset of the union of the sets of variables of each polynomial.
-/
theorem vars_prod {ι : Type*} [DecidableEq σ] {s : Finset ι} (f : ι → MvPolynomial σ R) :
(∏ i ∈ s, f i).vars ⊆ s.biUnion fun i => (f i).vars := by
classical
induction s using Finset.induction_on with
| empty => simp
| insert _ _ hs hsub =>
simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
apply Finset.Subset.trans (vars_mul _ _)
exact Finset.union_subset_union (Finset.Subset.refl _) hsub
