Def AlternatingMap.curryLeftLinearMap

Modification history

2025-06-04 03:03

Mathlib/LinearAlgebra/Alternating/Curry.lean

feat(AlternatingMap): define `AlternatingMap.uncurryFin`. (#25001)

Modified AlternatingMap.curryLeftLinearMap View on Github →

2025-05-12 19:31

Mathlib/LinearAlgebra/Alternating/Basic.lean

chore(LinearAlgebra/Alternating): move currying to a new file (#24800) …

Modified AlternatingMap.curryLeftLinearMap View on Github →

2023-04-10 15:18

Mathlib/LinearAlgebra/Alternating.lean

feat: port LinearAlgebra.Alternating (#3337)

Added AlternatingMap.curryLeftLinearMap View on Github →