Theorem MultilinearMap.domDomRestrict_apply

Modification history

2024-02-12 10:30

Mathlib/LinearAlgebra/Multilinear/Basic.lean

chore(LinearAlgebra/Multilinear): drop a `DecidableEq` assumption (#10437)

Modified MultilinearMap.domDomRestrict_apply View on Github →

2024-01-16 21:01

Mathlib/LinearAlgebra/Multilinear/Basic.lean

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

Added MultilinearMap.domDomRestrict_apply View on Github →