Theorem fderivWithin_continuousLinearEquiv_comp

Modification history

2024-05-06 12:00
Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
feat: the second derivative is the derivative of the derivative (#12697) …
Added fderivWithin_continuousLinearEquiv_compView on Github →