Commit 2020-09-22 11:28 caffd024

View on Github →

feat(data/polynomial/degree/trailing_degree): basic definitions and properties (#4113) Adds trailing_degree, trailing_nat_degree, trailing_coeff and various lemmas add functionality to work with trailing coefficients

Estimated changes

Created src/data/polynomial/degree/trailing_degree.lean

added theorem polynomial.coeff_eq_zero_of_lt_nat_trailing_degree

added theorem polynomial.coeff_eq_zero_of_trailing_degree_lt

added theorem polynomial.coeff_nat_trailing_degree_eq_zero_of_trailing_degree_lt

added theorem polynomial.coeff_nat_trailing_degree_pred_eq_zero

added theorem polynomial.le_trailing_degree_C

added theorem polynomial.le_trailing_degree_C_mul_X_pow

added theorem polynomial.le_trailing_degree_X

added theorem polynomial.le_trailing_degree_X_pow

added theorem polynomial.le_trailing_degree_of_ne_zero

added theorem polynomial.monomial_le_trailing_degree

added def polynomial.nat_trailing_degree

added theorem polynomial.nat_trailing_degree_C

added theorem polynomial.nat_trailing_degree_X

added theorem polynomial.nat_trailing_degree_X_le

added theorem polynomial.nat_trailing_degree_eq_of_trailing_degree_eq

added theorem polynomial.nat_trailing_degree_eq_of_trailing_degree_eq_some

added theorem polynomial.nat_trailing_degree_int_cast

added theorem polynomial.nat_trailing_degree_le_nat_trailing_degree

added theorem polynomial.nat_trailing_degree_le_of_ne_zero

added theorem polynomial.nat_trailing_degree_le_of_trailing_degree_le

added theorem polynomial.nat_trailing_degree_le_trailing_degree

added theorem polynomial.nat_trailing_degree_nat_cast

added theorem polynomial.nat_trailing_degree_neg

added theorem polynomial.nat_trailing_degree_one

added theorem polynomial.nat_trailing_degree_zero

added theorem polynomial.ne_zero_of_trailing_degree_lt

added def polynomial.next_coeff_up

added theorem polynomial.next_coeff_up_C_eq_zero

added theorem polynomial.next_coeff_up_of_pos_nat_trailing_degree

added def polynomial.trailing_coeff

added def polynomial.trailing_degree

added theorem polynomial.trailing_degree_C

added theorem polynomial.trailing_degree_X

added theorem polynomial.trailing_degree_eq_iff_nat_trailing_degree_eq

added theorem polynomial.trailing_degree_eq_iff_nat_trailing_degree_eq_of_pos

added theorem polynomial.trailing_degree_eq_nat_trailing_degree

added theorem polynomial.trailing_degree_eq_top

added theorem polynomial.trailing_degree_le_trailing_degree

added theorem polynomial.trailing_degree_lt_wf

added theorem polynomial.trailing_degree_monomial

added theorem polynomial.trailing_degree_ne_of_nat_trailing_degree_ne

added theorem polynomial.trailing_degree_neg

added theorem polynomial.trailing_degree_one

added theorem polynomial.trailing_degree_one_le

added theorem polynomial.trailing_degree_zero

added theorem polynomial.trailing_monic.def

added theorem polynomial.trailing_monic.trailing_coeff

added def polynomial.trailing_monic