Commit 2021-11-11 19:35 a9c3ab5d

View on Github →

feat(data/polynomial): assorted lemmas on division and gcd of polynomials (#9600) This PR provides a couple of lemmas involving the division and gcd operators of polynomials that I needed for #9563. The ones that generalized to euclidean_domain and/or gcd_monoid are provided in the respective files.

Estimated changes

Modified src/algebra/euclidean_domain.lean

added theorem euclidean_domain.div_dvd_of_dvd

added theorem euclidean_domain.div_one

added theorem euclidean_domain.mul_div_mul_cancel

Modified src/data/polynomial/field_division.lean

added theorem polynomial.C_mul_dvd

added theorem polynomial.div_C_mul

added theorem polynomial.dvd_C_mul

added theorem polynomial.leading_coeff_div

Modified src/ring_theory/euclidean_domain.lean

added theorem left_div_gcd_ne_zero

added theorem right_div_gcd_ne_zero

Modified src/ring_theory/polynomial/content.lean

added theorem polynomial.degree_gcd_le_left

added theorem polynomial.degree_gcd_le_right