Commit 2024-01-14 15:42 716dfd4a

View on Github →

feat: Lemmas relating Polynomial.eraseLead and nextCoeff. (#9083) Some little theorems relating eraseLead and nextCoeff to each other. Also includes monomial_sub and card_support_mul which could be of independent interest.

Estimated changes

Modified Mathlib/Data/Nat/SuccPred.lean

added theorem Nat.le_succ_iff_eq_or_le

Modified Mathlib/Data/Polynomial/Basic.lean

added theorem Polynomial.monomial_sub

Modified Mathlib/Data/Polynomial/Coeff.lean

added theorem Polynomial.card_support_mul_le

modified theorem Polynomial.isRegular_X

modified theorem Polynomial.isRegular_X_pow

Modified Mathlib/Data/Polynomial/Degree/Definitions.lean

added theorem Polynomial.natDegree_eq_zero

added theorem Polynomial.natDegree_le_pred

added theorem Polynomial.nextCoeff_eq_zero

added theorem Polynomial.nextCoeff_ne_zero

added theorem Polynomial.nextCoeff_of_natDegree_pos

deleted theorem Polynomial.nextCoeff_of_pos_natDegree

Modified Mathlib/Data/Polynomial/Degree/Lemmas.lean

added theorem Polynomial.natDegree_eq_one

added theorem Polynomial.natDegree_pos_of_nextCoeff_ne_zero

added theorem Polynomial.nextCoeff_C_mul_X_add_C

Modified Mathlib/Data/Polynomial/EraseLead.lean

added theorem Polynomial.card_support_eq_one_of_eraseLead_eq_zero

added theorem Polynomial.card_support_eraseLead'

added theorem Polynomial.card_support_eraseLead

added theorem Polynomial.card_support_eraseLead_add_one

added theorem Polynomial.card_support_le_one_of_eraseLead_eq_zero

added theorem Polynomial.eraseLead_C_mul_X

deleted theorem Polynomial.eraseLead_card_support'

deleted theorem Polynomial.eraseLead_card_support

added theorem Polynomial.leadingCoeff_eraseLead_eq_nextCoeff

added theorem Polynomial.natDegree_eraseLead

added theorem Polynomial.natDegree_eraseLead_add_one

added theorem Polynomial.natDegree_eraseLead_le_of_nextCoeff_eq_zero

added theorem Polynomial.natDegree_pos_of_eraseLead_ne_zero

added theorem Polynomial.nextCoeff_eq_zero_of_eraseLead_eq_zero

added theorem Polynomial.two_le_natDegree_of_nextCoeff_eraseLead

Modified Mathlib/RingTheory/Trace.lean

Modified test/RewriteSearch/Polynomial.lean