Commit 2023-03-24 20:19 31b48701

View on Github →

feat: port RingTheory.Polynomial.Content (#3066)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/Content.lean

added theorem Polynomial.C_content_dvd

added theorem Polynomial.IsPrimitive.content_eq_one

added theorem Polynomial.IsPrimitive.dvd_primPart_iff_dvd

added theorem Polynomial.IsPrimitive.mul

added theorem Polynomial.IsPrimitive.ne_zero

added theorem Polynomial.IsPrimitive.primPart_eq

added def Polynomial.IsPrimitive

added theorem Polynomial.Monic.isPrimitive

added theorem Polynomial.aeval_primPart_eq_zero

added def Polynomial.content

added theorem Polynomial.content_C

added theorem Polynomial.content_C_mul

added theorem Polynomial.content_X

added theorem Polynomial.content_X_mul

added theorem Polynomial.content_X_pow

added theorem Polynomial.content_dvd_coeff

added theorem Polynomial.content_eq_gcd_leadingCoeff_content_eraseLead

added theorem Polynomial.content_eq_gcd_range_of_lt

added theorem Polynomial.content_eq_gcd_range_succ

added theorem Polynomial.content_eq_zero_iff

added theorem Polynomial.content_monomial

added theorem Polynomial.content_mul

added theorem Polynomial.content_mul_aux

added theorem Polynomial.content_one

added theorem Polynomial.content_primPart

added theorem Polynomial.content_zero

added theorem Polynomial.degree_gcd_le_left

added theorem Polynomial.degree_gcd_le_right

added theorem Polynomial.dvd_content_iff_C_dvd

added theorem Polynomial.dvd_iff_content_dvd_content_and_primPart_dvd_primPart

added theorem Polynomial.eq_C_content_mul_primPart

added theorem Polynomial.eval₂_primPart_eq_zero

added theorem Polynomial.exists_primitive_lcm_of_isPrimitive

added theorem Polynomial.gcd_content_eq_of_dvd_sub

added theorem Polynomial.isPrimitive_iff_content_eq_one

added theorem Polynomial.isPrimitive_iff_isUnit_of_c_dvd

added theorem Polynomial.isPrimitive_of_dvd

added theorem Polynomial.isPrimitive_one

added theorem Polynomial.isPrimitive_primPart

added theorem Polynomial.isUnit_primPart_C

added theorem Polynomial.natDegree_primPart

added theorem Polynomial.normUnit_content

added theorem Polynomial.normalize_content

added theorem Polynomial.primPart_dvd

added theorem Polynomial.primPart_mul

added theorem Polynomial.primPart_ne_zero

added theorem Polynomial.primPart_zero