Commit 2020-10-24 05:36 de6a9d41

View on Github →

feat(ring_theory/polynomial/content): gcd_monoid instance on polynomials over gcd domain (#4760) Refactors ring_theory/polynomial/content a bit to introduce prim_part Provides a gcd_monoid instance on polynomials over a gcd domain

Estimated changes

Created src/data/polynomial/cancel_leads.lean

added def polynomial.cancel_leads

added theorem polynomial.dvd_cancel_leads_of_dvd_of_dvd

added theorem polynomial.nat_degree_cancel_leads_lt_of_nat_degree_le_nat_degree

added theorem polynomial.neg_cancel_leads

Modified src/ring_theory/polynomial/content.lean

added theorem polynomial.content_prim_part

added theorem polynomial.dvd_iff_content_dvd_content_and_prim_part_dvd_prim_part

added theorem polynomial.eq_C_content_mul_prim_part

deleted theorem polynomial.eq_C_mul_primitive

added theorem polynomial.exists_primitive_lcm_of_is_primitive

added theorem polynomial.is_primitive.dvd_prim_part_iff_dvd

added theorem polynomial.is_primitive.mul

added theorem polynomial.is_primitive.prim_part_eq

added theorem polynomial.is_primitive_prim_part

added theorem polynomial.is_unit_prim_part_C

added theorem polynomial.nat_degree_prim_part

added def polynomial.prim_part

added theorem polynomial.prim_part_dvd

added theorem polynomial.prim_part_mul

added theorem polynomial.prim_part_ne_zero

added theorem polynomial.prim_part_zero