Theorem MultilinearMap.directSum_ext

Modification history

2025-12-05 19:18

Mathlib/LinearAlgebra/Multilinear/DirectSum.lean

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

Added MultilinearMap.directSum_ext View on Github →