Lemmas about ideals of mv_polynomial #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Notably this contains results about monomial ideals.
Main results #
theorem
mv_polynomial.mem_ideal_span_monomial_image
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
{x : mv_polynomial σ R}
{s : set (σ →₀ ℕ)} :
x is in a monomial ideal generated by s iff every element of of its support dominates one of
the generators. Note that si ≤ xi is analogous to saying that the monomial corresponding to si
divides the monomial corresponding to xi.
theorem
mv_polynomial.mem_ideal_span_monomial_image_iff_dvd
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
{x : mv_polynomial σ R}
{s : set (σ →₀ ℕ)} :
x ∈ ideal.span ((λ (s : σ →₀ ℕ), ⇑(mv_polynomial.monomial s) 1) '' s) ↔ ∀ (xi : σ →₀ ℕ), xi ∈ x.support → (∃ (si : σ →₀ ℕ) (H : si ∈ s), ⇑(mv_polynomial.monomial si) 1 ∣ ⇑(mv_polynomial.monomial xi) (mv_polynomial.coeff xi x))
theorem
mv_polynomial.mem_ideal_span_X_image
{σ : Type u_1}
{R : Type u_2}
[comm_semiring R]
{x : mv_polynomial σ R}
{s : set σ} :
x is in a monomial ideal generated by variables X iff every element of of its support
has a component in s.