Def MultilinearMap.linearDeriv

Modification history

2024-01-16 21:01

Mathlib/LinearAlgebra/Multilinear/Basic.lean

feat(LinearAlgebra/Multilinear/Basic): derivative of a multilinear map (#9130) …

Added MultilinearMap.linearDeriv View on Github →