Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-22 10:05 57e09a12

View on Github →

feat(algebra/monoid_algebra): add division by a generator (#15905) This generalizes polynomial.div_X. Zulip thread

Estimated changes

Modified src/algebra/monoid_algebra/basic.lean

added theorem add_monoid_algebra.mul_single_apply_of_not_exists_add

added theorem add_monoid_algebra.single_mul_apply_of_not_exists_add

added theorem monoid_algebra.mul_single_apply_of_not_exists_mul

added theorem monoid_algebra.single_mul_apply_of_not_exists_mul

Created src/algebra/monoid_algebra/division.lean

added theorem add_monoid_algebra.add_div_of

added theorem add_monoid_algebra.div_of_add

added theorem add_monoid_algebra.div_of_add_mod_of

added theorem add_monoid_algebra.div_of_apply

added theorem add_monoid_algebra.div_of_zero

added theorem add_monoid_algebra.mod_of_add_div_of

added theorem add_monoid_algebra.mod_of_apply_add_self

added theorem add_monoid_algebra.mod_of_apply_of_exists_add

added theorem add_monoid_algebra.mod_of_apply_of_not_exists_add

added theorem add_monoid_algebra.mod_of_apply_self_add

added theorem add_monoid_algebra.mul_of'_div_of

added theorem add_monoid_algebra.mul_of'_mod_of

added theorem add_monoid_algebra.of'_div_of

added theorem add_monoid_algebra.of'_mod_of

added theorem add_monoid_algebra.of'_mul_div_of

added theorem add_monoid_algebra.of'_mul_mod_of

added theorem add_monoid_algebra.support_div_of

added theorem add_monoid_algebra.zero_div_of

Created src/data/mv_polynomial/division.lean

added theorem mv_polynomial.X_div_monomial

added theorem mv_polynomial.X_mul_div_monomial

added theorem mv_polynomial.X_mul_mod_monomial

added theorem mv_polynomial.add_div_monomial

added theorem mv_polynomial.coeff_div_monomial

added theorem mv_polynomial.coeff_mod_monomial_of_le

added theorem mv_polynomial.coeff_mod_monomial_of_not_le

added theorem mv_polynomial.div_monomial_add

added theorem mv_polynomial.div_monomial_add_mod_monomial

added theorem mv_polynomial.div_monomial_add_mod_monomial_single

added theorem mv_polynomial.div_monomial_monomial

added theorem mv_polynomial.div_monomial_monomial_mul

added theorem mv_polynomial.div_monomial_mul_monomial

added theorem mv_polynomial.div_monomial_zero

added theorem mv_polynomial.mod_monomial_X

added theorem mv_polynomial.mod_monomial_add_div_monomial

added theorem mv_polynomial.mod_monomial_add_div_monomial_single

added theorem mv_polynomial.monomial_mod_monomial

added theorem mv_polynomial.monomial_mul_mod_monomial

added theorem mv_polynomial.mul_X_div_monomial

added theorem mv_polynomial.mul_X_mod_monomial

added theorem mv_polynomial.mul_monomial_mod_monomial

added theorem mv_polynomial.support_div_monomial

added theorem mv_polynomial.zero_div_monomial

Modified src/data/polynomial/inductions.lean