Commit 2024-05-06 12:00 8ea47a76

View on Github →

feat: the second derivative is the derivative of the derivative (#12697) Also expand a little bit the API and some cleanups.

Estimated changes

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

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

added theorem iteratedFDerivWithin_two_apply

added theorem iteratedFDerivWithin_zero_eq

added theorem iteratedFDeriv_two_apply

deleted theorem iteratedFDeriv_with_zero_eq

Modified Mathlib/Analysis/Calculus/FDeriv/Equiv.lean

added theorem LinearIsometryEquiv.comp_fderiv'

added theorem fderivWithin_continuousLinearEquiv_comp

added theorem fderiv_continuousLinearEquiv_comp'

added theorem fderiv_continuousLinearEquiv_comp

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

added theorem ContinuousLinearEquiv.arrowCongr_apply

added theorem ContinuousLinearEquiv.arrowCongr_symm