Commit 2026-02-19 13:50 8bd514e0

View on Github →

feat: iterated derivatives of differences of functions (#35256) Establish standard formulas for iterated derivatives of differences of functions. Change the names of theorems to comply with style standards.

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Operations.lean

deleted theorem iteratedFDerivWithin_add_apply'

modified theorem iteratedFDerivWithin_add_apply

added theorem iteratedFDerivWithin_sub_apply

modified theorem iteratedFDeriv_add

deleted theorem iteratedFDeriv_add_apply'

modified theorem iteratedFDeriv_add_apply

added theorem iteratedFDeriv_sub

added theorem iteratedFDeriv_sub_apply