Commit 2024-12-18 13:24 cbe8d43a

View on Github →

feat: add some iteratedDeriv variants of iteratedDerivWithin lemmas (#19849) Based on work from EulerMaclaurin.

Estimated changes

Modified Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean

deleted theorem iteratedDerivWithin_const_neg

added theorem iteratedDerivWithin_const_sub

added theorem iteratedDeriv_add

added theorem iteratedDeriv_const_add

added theorem iteratedDeriv_const_sub

added theorem iteratedDeriv_sub