English
Characterization of membership in the ideal span of monomials: x ∈ span({monomial s (1) : s ∈ S}) iff every monomial in x’s support is bounded above by some s ∈ S in the monomial order.
Русский
Характеризация принадлежности x к идеалу, порождаемому мономами: x ∈ span({monomial s (1) : s ∈ S}) тогда и только тогда, когда каждая мономиальная компонент в поддержке x ограничена некоторым s ∈ S по порядку мономов.
LaTeX
$$(homogeneousComponent n φ) ∈ …$$
Lean4
theorem mem_ideal_span_monomial_image_iff_dvd {x : MvPolynomial σ R} {s : Set (σ →₀ ℕ)} :
x ∈ Ideal.span ((fun s => monomial s (1 : R)) '' s) ↔
∀ xi ∈ x.support, ∃ si ∈ s, monomial si 1 ∣ monomial xi (x.coeff xi) :=
by
refine mem_ideal_span_monomial_image.trans (forall₂_congr fun xi hxi => ?_)
simp_rw [monomial_dvd_monomial, one_dvd, and_true, mem_support_iff.mp hxi, false_or]