Mathlib Changelog
v4
Changelog
About
Github
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