Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-02 00:24 5eb7ebbb

View on Github →

feat(data/polynomial): lemmas about polynomial derivative (#6433)

Estimated changes

Modified src/data/polynomial/algebra_map.lean

deleted theorem polynomial.pow_comp

Modified src/data/polynomial/derivative.lean

added theorem polynomial.derivative_C_mul

added theorem polynomial.derivative_cast_nat

added theorem polynomial.derivative_comp

added def polynomial.derivative_lhom

added theorem polynomial.derivative_lhom_coe

modified theorem polynomial.derivative_sub

added theorem polynomial.iterate_derivative_C_mul

added theorem polynomial.iterate_derivative_add

added theorem polynomial.iterate_derivative_cast_nat_mul

added theorem polynomial.iterate_derivative_map

added theorem polynomial.iterate_derivative_neg

added theorem polynomial.iterate_derivative_smul

added theorem polynomial.iterate_derivative_sub

added theorem polynomial.iterate_derivative_zero

Modified src/data/polynomial/eval.lean

added theorem polynomial.cast_int_comp

added theorem polynomial.cast_nat_comp

added theorem polynomial.monomial_comp

added theorem polynomial.pow_comp