The derivative of bounded linear maps #
For detailed documentation of the Fréchet derivative,
see the module docstring of
This file contains the usual formulas (and existence assertions) for the derivative of bounded linear maps.
Continuous linear maps #
There are currently two variants of these in mathlib, the bundled version
ContinuousLinearMap, and denoted
E →L[𝕜] F), and the unbundled version (with a
IsBoundedLinearMap). We give statements for both versions.