Def MultilinearMap.compLinearMapMultilinear

Modification history

2023-11-28 20:10

Mathlib/LinearAlgebra/Multilinear/Basic.lean

feat: multilinearity of the `MultilinearMap.compLinearMap` operation (#8684)

Added MultilinearMap.compLinearMapMultilinear View on Github →