The derivative of bounded bilinear maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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 bilinear maps.
Derivative of a bounded bilinear map #