# Lemmas about ideals of `MvPolynomial`

#

Notably this contains results about monomial ideals.

## Main results #

theorem
MvPolynomial.mem_ideal_span_monomial_image
{σ : Type u_1}
{R : Type u_2}
[CommSemiring R]
{x : MvPolynomial σ R}
{s : Set (σ →₀ ℕ)}
:

x ∈ Ideal.span ((fun s => ↑(MvPolynomial.monomial s) 1) '' s) ↔ ∀ (xi : σ →₀ ℕ), xi ∈ MvPolynomial.support x → ∃ si, si ∈ s ∧ si ≤ xi

`x`

is in a monomial ideal generated by `s`

iff every element 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
MvPolynomial.mem_ideal_span_monomial_image_iff_dvd
{σ : Type u_1}
{R : Type u_2}
[CommSemiring R]
{x : MvPolynomial σ R}
{s : Set (σ →₀ ℕ)}
:

x ∈ Ideal.span ((fun s => ↑(MvPolynomial.monomial s) 1) '' s) ↔ ∀ (xi : σ →₀ ℕ),
xi ∈ MvPolynomial.support x →
∃ si, si ∈ s ∧ ↑(MvPolynomial.monomial si) 1 ∣ ↑(MvPolynomial.monomial xi) (MvPolynomial.coeff xi x)

theorem
MvPolynomial.mem_ideal_span_X_image
{σ : Type u_1}
{R : Type u_2}
[CommSemiring R]
{x : MvPolynomial σ R}
{s : Set σ}
:

`x`

is in a monomial ideal generated by variables `X`

iff every element of its support
has a component in `s`

.