Commit 2025-01-07 19:57 f100ec8b

View on Github →

feat(ContDiff): add iteratedFDeriv_comp (#20472)

Estimated changes

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

added theorem iteratedFDerivWithin_comp

added theorem iteratedFDerivWithin_comp_of_eventually_mem

added theorem iteratedFDeriv_comp

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

added theorem ContDiffWithinAt.eventually_hasFTaylorSeriesUpToOn