Commit 2024-03-29 10:05 3b9115ff

View on Github →

feat(Polynomial): When the trailing degree is zero (#11655) Characterise when trailingDegree p = 0 and natTrailingDegree p = 0. Also fix a few names.

Estimated changes

Modified Mathlib/Data/Polynomial/Basic.lean

added theorem Polynomial.support_nonempty

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

added theorem Polynomial.coeff_eq_zero_of_lt_trailingDegree

deleted theorem Polynomial.coeff_eq_zero_of_trailingDegree_lt

added theorem Polynomial.coeff_natTrailingDegree_eq_zero

added theorem Polynomial.coeff_natTrailingDegree_ne_zero

deleted theorem Polynomial.le_trailingDegree_of_ne_zero

added theorem Polynomial.natTrailingDegree_eq_zero

added theorem Polynomial.natTrailingDegree_ne_zero

added theorem Polynomial.nextCoeffUp_of_constantCoeff_eq_zero

deleted theorem Polynomial.nextCoeffUp_of_pos_natTrailingDegree

added theorem Polynomial.nextCoeffUp_zero

added theorem Polynomial.trailingDegree_eq_zero

added theorem Polynomial.trailingDegree_le_of_ne_zero

modified theorem Polynomial.trailingDegree_le_trailingDegree

added theorem Polynomial.trailingDegree_ne_zero

Modified Mathlib/Data/Polynomial/Mirror.lean

Modified Mathlib/Data/Polynomial/Reverse.lean

added theorem Polynomial.natTrailingDegree_reverse

deleted theorem Polynomial.reverse_natTrailingDegree

Modified Mathlib/Data/Polynomial/UnitTrinomial.lean