Theorem LinearIsometryEquiv.comp_fderiv'

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 LinearIsometryEquiv.comp_fderiv'View on Github →