Commit 2023-03-27 12:09 7c5a5330

View on Github →

feat: port Data.MvPolynomial.Division (#3100)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/MvPolynomial/Division.lean

added theorem MvPolynomial.add_divMonomial

added theorem MvPolynomial.coeff_divMonomial

added theorem MvPolynomial.coeff_modMonomial_of_le

added theorem MvPolynomial.coeff_modMonomial_of_not_le

added theorem MvPolynomial.divMonomial_add

added theorem MvPolynomial.divMonomial_add_modMonomial

added theorem MvPolynomial.divMonomial_add_modMonomial_single

added theorem MvPolynomial.divMonomial_monomial

added theorem MvPolynomial.divMonomial_monomial_mul

added theorem MvPolynomial.divMonomial_mul_monomial

added theorem MvPolynomial.divMonomial_zero

added theorem MvPolynomial.modMonomial_add_divMonomial

added theorem MvPolynomial.modMonomial_add_divMonomial_single

added theorem MvPolynomial.modMonomial_x

added theorem MvPolynomial.monomial_dvd_monomial

added theorem MvPolynomial.monomial_modMonomial

added theorem MvPolynomial.monomial_mul_modMonomial

added theorem MvPolynomial.monomial_one_dvd_iff_modMonomial_eq_zero

added theorem MvPolynomial.monomial_one_dvd_monomial_one

added theorem MvPolynomial.mul_monomial_modMonomial

added theorem MvPolynomial.mul_x_divMonomial

added theorem MvPolynomial.mul_x_modMonomial

added theorem MvPolynomial.support_divMonomial

added theorem MvPolynomial.x_divMonomial

added theorem MvPolynomial.x_dvd_iff_modMonomial_eq_zero

added theorem MvPolynomial.x_dvd_monomial

added theorem MvPolynomial.x_dvd_x

added theorem MvPolynomial.x_mul_divMonomial

added theorem MvPolynomial.x_mul_modMonomial

added theorem MvPolynomial.zero_divMonomial