Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-09 15:47 4a15eddd

View on Github →

feat(data/polynomial/monic): monic.not_zero_divisor_iff (#8417) We prove that a monic polynomial is not a zero divisor. A helper lemma is proven that the product of a monic polynomial is of lesser degree iff it is nontrivial and the multiplicand is zero.

Estimated changes

Modified src/data/polynomial/degree/definitions.lean

modified theorem polynomial.degree_mul_X

deleted theorem polynomial.degree_mul_monic

added theorem polynomial.monic.degree_mul

Modified src/data/polynomial/div.lean

Modified src/data/polynomial/monic.lean

added theorem polynomial.degree_smul_of_non_zero_divisor

added theorem polynomial.is_unit_leading_coeff_mul_left_eq_zero_iff

added theorem polynomial.is_unit_leading_coeff_mul_right_eq_zero_iff

added theorem polynomial.leading_coeff_smul_of_non_zero_divisor

deleted theorem polynomial.monic.degree_eq_zero_iff_eq_one

added theorem polynomial.monic.degree_le_zero_iff_eq_one

added theorem polynomial.monic.degree_mul_comm

added theorem polynomial.monic.mul_left_eq_zero_iff

added theorem polynomial.monic.mul_left_ne_zero

added theorem polynomial.monic.mul_nat_degree_lt_iff

added theorem polynomial.monic.mul_right_eq_zero_iff

added theorem polynomial.monic.mul_right_ne_zero

added theorem polynomial.monic.nat_degree_eq_zero_iff_eq_one

added theorem polynomial.monic.nat_degree_mul'

added theorem polynomial.monic.nat_degree_mul_comm

added theorem polynomial.monic_C_mul_of_mul_leading_coeff_eq_one

added theorem polynomial.monic_of_is_unit_leading_coeff_inv_smul

added theorem polynomial.nat_degree_smul_of_non_zero_divisor