# Documentation

Mathlib.RingTheory.MvPolynomial.Ideal

# Lemmas about ideals of MvPolynomial#

Notably this contains results about monomial ideals.

## Main results #

• MvPolynomial.mem_ideal_span_monomial_image
• MvPolynomial.mem_ideal_span_X_image
theorem MvPolynomial.mem_ideal_span_monomial_image {σ : Type u_1} {R : Type u_2} [] {x : } {s : Set (σ →₀ )} :
x Ideal.span ((fun s => ↑() 1) '' s) ∀ (xi : σ →₀ ), 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} [] {x : } {s : Set (σ →₀ )} :
x Ideal.span ((fun s => ↑() 1) '' s) ∀ (xi : σ →₀ ), si, si s ↑() 1 ↑() ()
theorem MvPolynomial.mem_ideal_span_X_image {σ : Type u_1} {R : Type u_2} [] {x : } {s : Set σ} :
x Ideal.span (MvPolynomial.X '' s) ∀ (m : σ →₀ ), i, i s m i 0

x is in a monomial ideal generated by variables X iff every element of its support has a component in s.