Theorem AlternatingMap.uncurryFin_curryLeft

Modification history

2025-10-04 09:36
Mathlib/LinearAlgebra/Alternating/Uncurry/Fin.lean
feat(NormedSpace/Alternating/Uncurry/Fin): new file (#29957)
Deleted AlternatingMap.uncurryFin_curryLeftView on Github →
2025-06-04 03:03
Mathlib/LinearAlgebra/Alternating/Uncurry/Fin.lean
feat(AlternatingMap): define `AlternatingMap.uncurryFin`. (#25001)
Added AlternatingMap.uncurryFin_curryLeftView on Github →