Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-23 11:10 ecd889a5

View on Github →

feat(data/polynomial/*): higher order derivative (#4187)

Estimated changes

Created src/data/polynomial/iterated_deriv.lean

added theorem polynomial.coeff_iterated_deriv_as_prod_Ico

added theorem polynomial.coeff_iterated_deriv_as_prod_range

added def polynomial.iterated_deriv

added theorem polynomial.iterated_deriv_C

added theorem polynomial.iterated_deriv_C_zero

added theorem polynomial.iterated_deriv_X

added theorem polynomial.iterated_deriv_X_one

added theorem polynomial.iterated_deriv_X_zero

added theorem polynomial.iterated_deriv_add

added theorem polynomial.iterated_deriv_eq_zero_of_nat_degree_lt

added theorem polynomial.iterated_deriv_mul

added theorem polynomial.iterated_deriv_neg

added theorem polynomial.iterated_deriv_one

added theorem polynomial.iterated_deriv_one_zero

added theorem polynomial.iterated_deriv_smul

added theorem polynomial.iterated_deriv_sub

added theorem polynomial.iterated_deriv_succ

added theorem polynomial.iterated_deriv_zero_left

added theorem polynomial.iterated_deriv_zero_right