Def ContinuousMultilinearMap.linearDeriv

Modification history

2024-02-06 18:38

Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean

feat: define `ContinuousMultilinearMap.linearDeriv` and show it's the `fderiv` (#9846)

Added ContinuousMultilinearMap.linearDeriv View on Github →