Commit 2023-03-08 17:48 f89ee530

View on Github →

feat: port Data.Polynomial.Degree.TrailingDegree (#2722)

Estimated changes

Modified Mathlib.lean

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

added theorem Polynomial.TrailingMonic.def

added theorem Polynomial.TrailingMonic.trailingCoeff

added def Polynomial.TrailingMonic

added theorem Polynomial.coeff_eq_zero_of_lt_natTrailingDegree

added theorem Polynomial.coeff_eq_zero_of_trailingDegree_lt

added theorem Polynomial.coeff_mul_natTrailingDegree_add_natTrailingDegree

added theorem Polynomial.coeff_natTrailingDegree_eq_zero_of_trailingDegree_lt

added theorem Polynomial.coeff_natTrailingDegree_pred_eq_zero

added theorem Polynomial.le_natTrailingDegree

added theorem Polynomial.le_natTrailingDegree_mul

added theorem Polynomial.le_trailingDegree_C

added theorem Polynomial.le_trailingDegree_C_mul_X_pow

added theorem Polynomial.le_trailingDegree_X

added theorem Polynomial.le_trailingDegree_X_pow

added theorem Polynomial.le_trailingDegree_monomial

added theorem Polynomial.le_trailingDegree_mul

added theorem Polynomial.le_trailingDegree_of_ne_zero

added def Polynomial.natTrailingDegree

added theorem Polynomial.natTrailingDegree_C

added theorem Polynomial.natTrailingDegree_X

added theorem Polynomial.natTrailingDegree_X_le

added theorem Polynomial.natTrailingDegree_eq_of_trailingDegree_eq

added theorem Polynomial.natTrailingDegree_eq_of_trailingDegree_eq_some

added theorem Polynomial.natTrailingDegree_eq_support_min'

added theorem Polynomial.natTrailingDegree_int_cast

added theorem Polynomial.natTrailingDegree_le_natDegree

added theorem Polynomial.natTrailingDegree_le_natTrailingDegree

added theorem Polynomial.natTrailingDegree_le_of_mem_supp

added theorem Polynomial.natTrailingDegree_le_of_ne_zero

added theorem Polynomial.natTrailingDegree_le_of_trailingDegree_le

added theorem Polynomial.natTrailingDegree_le_trailingDegree

added theorem Polynomial.natTrailingDegree_mem_support_of_nonzero

added theorem Polynomial.natTrailingDegree_monomial

added theorem Polynomial.natTrailingDegree_monomial_le

added theorem Polynomial.natTrailingDegree_mul'

added theorem Polynomial.natTrailingDegree_mul

added theorem Polynomial.natTrailingDegree_mul_X_pow

added theorem Polynomial.natTrailingDegree_nat_cast

added theorem Polynomial.natTrailingDegree_neg

added theorem Polynomial.natTrailingDegree_one

added theorem Polynomial.natTrailingDegree_zero

added theorem Polynomial.ne_zero_of_trailingDegree_lt

added def Polynomial.nextCoeffUp

added theorem Polynomial.nextCoeffUp_C_eq_zero

added theorem Polynomial.nextCoeffUp_of_pos_natTrailingDegree

added def Polynomial.trailingCoeff

added theorem Polynomial.trailingCoeff_eq_zero

added theorem Polynomial.trailingCoeff_nonzero_iff_nonzero

added theorem Polynomial.trailingCoeff_zero

added def Polynomial.trailingDegree

added theorem Polynomial.trailingDegree_C

added theorem Polynomial.trailingDegree_C_mul_X_pow

added theorem Polynomial.trailingDegree_X

added theorem Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq

added theorem Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq_of_pos

added theorem Polynomial.trailingDegree_eq_natTrailingDegree

added theorem Polynomial.trailingDegree_eq_top

added theorem Polynomial.trailingDegree_le_trailingDegree

added theorem Polynomial.trailingDegree_lt_wf

added theorem Polynomial.trailingDegree_monomial

added theorem Polynomial.trailingDegree_mul'

added theorem Polynomial.trailingDegree_ne_of_natTrailingDegree_ne

added theorem Polynomial.trailingDegree_neg

added theorem Polynomial.trailingDegree_one

added theorem Polynomial.trailingDegree_one_le

added theorem Polynomial.trailingDegree_zero