# mathlib3documentation

ring_theory.mv_polynomial.ideal

# 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 #

• mv_polynomial.mem_ideal_span_monomial_image
• mv_polynomial.mem_ideal_span_X_image
theorem mv_polynomial.mem_ideal_span_monomial_image {σ : Type u_1} {R : Type u_2} {x : R} {s : set →₀ )} :
x ideal.span ((λ (s : σ →₀ ), 1) '' s) (xi : σ →₀ ), xi x.support ( (si : σ →₀ ) (H : si s), si xi)

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} {x : R} {s : set →₀ )} :
x ideal.span ((λ (s : σ →₀ ), 1) '' s) (xi : σ →₀ ), xi x.support ( (si : σ →₀ ) (H : si s), 1 x))
theorem mv_polynomial.mem_ideal_span_X_image {σ : Type u_1} {R : Type u_2} {x : R} {s : set σ} :
x (m : σ →₀ ), m x.support ( (i : σ) (H : i s), m i 0)

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