Commit 2025-02-27 06:14 0d00ffcd
View on Github →chore: split Mathlib.LinearAlgebra.Multilinear.Basic (#22350) There's a straightforward split to get under the long file limit, by moving the material on currying to its own file.
chore: split Mathlib.LinearAlgebra.Multilinear.Basic (#22350) There's a straightforward split to get under the long file limit, by moving the material on currying to its own file.