Theorem LinearMap.id_compMultilinearMap

Modification history

2026-10-29 21:19
Mathlib/LinearAlgebra/Multilinear/Basic.lean
feat(LinearAlgebra/MultilinearMap): notation for `MultilinearMap` (#43877) …
Modified LinearMap.id_compMultilinearMapView on Github →
2025-05-29 13:58
Mathlib/LinearAlgebra/Multilinear/Basic.lean
feat: associativity lemmas for `MultilinearMap` composition (#25169) …
Added LinearMap.id_compMultilinearMapView on Github →