mem_ideal_span_monomial_image_iff_dvd

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]

Похожие утверждения