Theorem fderiv_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 fderiv_continuousLinearEquiv_comp'View on Github →