Def LinearMap.uncurryLeft

Modification history

2026-10-29 21:19

Mathlib/LinearAlgebra/Multilinear/Curry.lean

feat(LinearAlgebra/MultilinearMap): notation for `MultilinearMap` (#43877) …

Modified LinearMap.uncurryLeft View on Github →

2025-02-27 06:14

Mathlib/LinearAlgebra/Multilinear/Basic.lean

chore: split Mathlib.LinearAlgebra.Multilinear.Basic (#22350) …

Modified LinearMap.uncurryLeft View on Github →

2023-04-07 11:39

Mathlib/LinearAlgebra/Multilinear/Basic.lean

feat: port LinearAlgebra.Multilinear.Basic (#2450)

Added LinearMap.uncurryLeft View on Github →