Commit 2024-01-16 21:01 fc4c73bb

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

• Define the derivative f.linearDeriv of a multilinear map f at x, i.e. the first-order term of f(x+h)-f(x+h').
• Define MultilinearMap.domDomRestrict: given a multilinear map indexed by a type ι, a function P: ι → Prop and a vector z define on {a // ¬ P a}, this is the multilinear map indexed by {a // P a} sending x to the value of f at the vector that has coordinate at a : ι equal to x a if P a and z a if ¬ P a.
• depends on: #9137