Theorem MultilinearMap.fromDirectSumEquiv_symm_apply

Modification history

2025-12-05 19:18

Mathlib/LinearAlgebra/Multilinear/DirectSum.lean

feat(LinearAlgebra/Multilinear): constructing `MultilinearMap` over `DirectSum` (#32450) …

Added MultilinearMap.fromDirectSumEquiv_symm_apply View on Github →