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.

Estimated changes

Modified src/algebra/monoid_algebra/division.lean

added theorem add_monoid_algebra.of'_dvd_iff_mod_of_eq_zero

Created src/algebra/monoid_algebra/ideal.lean

added theorem add_monoid_algebra.mem_ideal_span_of'_image

added theorem monoid_algebra.mem_ideal_span_of_image

Modified src/data/mv_polynomial/division.lean

added theorem mv_polynomial.X_dvd_X

added theorem mv_polynomial.X_dvd_iff_mod_monomial_eq_zero

added theorem mv_polynomial.X_dvd_monomial

added theorem mv_polynomial.monomial_dvd_monomial

added theorem mv_polynomial.monomial_one_dvd_iff_mod_monomial_eq_zero

added theorem mv_polynomial.monomial_one_dvd_monomial_one

Created src/ring_theory/mv_polynomial/ideal.lean

added theorem mv_polynomial.mem_ideal_span_X_image

added theorem mv_polynomial.mem_ideal_span_monomial_image

added theorem mv_polynomial.mem_ideal_span_monomial_image_iff_dvd