Commit 2023-03-09 09:05 1e410886

View on Github →

feat: port Data.Polynomial.Derivative (#2725)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Ring/Basic.lean

Created Mathlib/Data/Polynomial/Derivative.lean

added theorem Polynomial.coeff_derivative

added theorem Polynomial.coeff_iterate_derivative_as_prod_Ico

added theorem Polynomial.coeff_iterate_derivative_as_prod_range

added theorem Polynomial.degree_derivative_eq

added theorem Polynomial.degree_derivative_le

added theorem Polynomial.degree_derivative_lt

added def Polynomial.derivative

added theorem Polynomial.derivative_C

added theorem Polynomial.derivative_C_mul_X

added theorem Polynomial.derivative_C_mul_X_pow

added theorem Polynomial.derivative_C_mul_X_sq

added theorem Polynomial.derivative_X

added theorem Polynomial.derivative_X_add_C

added theorem Polynomial.derivative_X_add_C_pow

added theorem Polynomial.derivative_X_add_C_sq

added theorem Polynomial.derivative_X_pow

added theorem Polynomial.derivative_X_sq

added theorem Polynomial.derivative_X_sub_C

added theorem Polynomial.derivative_X_sub_C_pow

added theorem Polynomial.derivative_X_sub_C_sq

added theorem Polynomial.derivative_add

added theorem Polynomial.derivative_apply

added theorem Polynomial.derivative_bit0

added theorem Polynomial.derivative_bit1

added theorem Polynomial.derivative_comp

added theorem Polynomial.derivative_comp_one_sub_X

added theorem Polynomial.derivative_eval

added theorem Polynomial.derivative_eval₂_C

added theorem Polynomial.derivative_int_cast

added theorem Polynomial.derivative_int_cast_mul

added theorem Polynomial.derivative_map

added theorem Polynomial.derivative_monomial

added theorem Polynomial.derivative_mul

added theorem Polynomial.derivative_nat_cast

added theorem Polynomial.derivative_nat_cast_mul

added theorem Polynomial.derivative_neg

added theorem Polynomial.derivative_of_natDegree_zero

added theorem Polynomial.derivative_one

added theorem Polynomial.derivative_pow

added theorem Polynomial.derivative_pow_succ

added theorem Polynomial.derivative_prod

added theorem Polynomial.derivative_smul

added theorem Polynomial.derivative_sq

added theorem Polynomial.derivative_sub

added theorem Polynomial.derivative_sum

added theorem Polynomial.derivative_zero

added theorem Polynomial.dvd_iterate_derivative_pow

added theorem Polynomial.eq_c_of_derivative_eq_zero

added theorem Polynomial.eval_multiset_prod_X_sub_C_derivative

added theorem Polynomial.iterate_derivative_C

added theorem Polynomial.iterate_derivative_C_mul

added theorem Polynomial.iterate_derivative_X_add_pow

added theorem Polynomial.iterate_derivative_X_pow_eq_C_mul

added theorem Polynomial.iterate_derivative_X_pow_eq_nat_cast_mul

added theorem Polynomial.iterate_derivative_X_pow_eq_smul

added theorem Polynomial.iterate_derivative_X_sub_pow

added theorem Polynomial.iterate_derivative_add

added theorem Polynomial.iterate_derivative_comp_one_sub_X

added theorem Polynomial.iterate_derivative_eq_zero

added theorem Polynomial.iterate_derivative_int_cast_mul

added theorem Polynomial.iterate_derivative_map

added theorem Polynomial.iterate_derivative_mul

added theorem Polynomial.iterate_derivative_nat_cast_mul

added theorem Polynomial.iterate_derivative_neg

added theorem Polynomial.iterate_derivative_one

added theorem Polynomial.iterate_derivative_smul

added theorem Polynomial.iterate_derivative_sub

added theorem Polynomial.iterate_derivative_x

added theorem Polynomial.iterate_derivative_zero

added theorem Polynomial.mem_support_derivative

added theorem Polynomial.natDegree_derivative_le

added theorem Polynomial.natDegree_derivative_lt

added theorem Polynomial.natDegree_eq_zero_of_derivative_eq_zero

added theorem Polynomial.of_mem_support_derivative