Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-30 16:44 1da31fac

View on Github →

feat(data/polynomial/derivative): add more lemmas (#16139)

Estimated changes

Modified src/data/polynomial/derivative.lean

added theorem polynomial.derivative_X_add_pow

added theorem polynomial.derivative_X_sub_pow

added theorem polynomial.derivative_int_cast

added theorem polynomial.derivative_int_cast_mul

added theorem polynomial.derivative_nat_cast_mul

added theorem polynomial.dvd_iterate_derivative_pow

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_int_cast_mul