mathlib3

72c366d0 - feat(ring_theory/mv_polynomial/ideal): lemmas about monomial ideals (#18633)

feat(ring_theory/mv_polynomial/ideal): lemmas about monomial ideals (#18633) Inspired by [this Zulip message](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.F0.9D.94.BD.E2.82.82.5B.CE.B1.2C.20.CE.B2.2C.20.CE.B3.5D.20.2F.20.28.CE.B1.C2.B2.2C.20.CE.B2.C2.B2.2C.20.CE.B3.C2.B2.29/near/292327061). Instead of defining `ideal_ge'` directly, we show results about the more natural spelling with `ideal.span`. This also adds a handful of results about `dvd` on `mv_polynomial`.