Commit 2023-03-23 23:41 72c366d0
View on Github →feat(ring_theory/mv_polynomial/ideal): lemmas about monomial ideals (#18633)
Inspired by this Zulip message. 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
.