Commit 2023-08-01 14:29 8dd13612

View on Github →

feat: n-th derivative of C^{n+p} map is C^p (#6101)

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff.lean

added theorem ContDiff.iteratedFDeriv_right

added theorem ContDiffAt.iteratedFDeriv_right

added theorem ContDiffWithinAt.iteratedFderivWithin_right

Modified Mathlib/Analysis/Calculus/ContDiffDef.lean

added theorem fderivWithin_iteratedFDerivWithin