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.

Author: kim-em

Mathlib.lean

@@ -3762,6 +3762,7 @@ import Mathlib.LinearAlgebra.Matrix.Transvection
 import Mathlib.LinearAlgebra.Matrix.ZPow
 import Mathlib.LinearAlgebra.Multilinear.Basic
 import Mathlib.LinearAlgebra.Multilinear.Basis
+import Mathlib.LinearAlgebra.Multilinear.Curry
 import Mathlib.LinearAlgebra.Multilinear.DFinsupp
 import Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
 import Mathlib.LinearAlgebra.Multilinear.Pi

Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import Mathlib.Analysis.NormedSpace.Multilinear.Basic
+import Mathlib.LinearAlgebra.Multilinear.Curry
 
 /-!
 # Currying and uncurrying continuous multilinear maps

Mathlib/LinearAlgebra/Multilinear/Basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
-import Mathlib.LinearAlgebra.Multilinear.Basic
+import Mathlib.LinearAlgebra.Multilinear.Curry
 import Mathlib.LinearAlgebra.Basis.Defs
 
 /-!

Mathlib/LinearAlgebra/Multilinear/Basis.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import Mathlib.LinearAlgebra.Multilinear.Basic
+import Mathlib.LinearAlgebra.Multilinear.Curry
 import Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
 
 /-! # Multilinear maps over finite dimensional spaces

Mathlib/LinearAlgebra/Multilinear/Curry.lean

@@ -3,8 +3,8 @@ Copyright (c) 2020 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.LinearAlgebra.Multilinear.Basic
 import Mathlib.LinearAlgebra.TensorProduct.Basic
+import Mathlib.LinearAlgebra.Multilinear.Basic
 
 /-!
 # Constructions relating multilinear maps and tensor products.

Mathlib/LinearAlgebra/Multilinear/FiniteDimensional.lean

@@ -5,6 +5,7 @@ Authors: Frédéric Dupuis, Eric Wieser
 -/
 import Mathlib.LinearAlgebra.Multilinear.TensorProduct
 import Mathlib.Tactic.AdaptationNote
+import Mathlib.LinearAlgebra.Multilinear.Curry
 
 /-!
 # Tensor product of an indexed family of modules over commutative semirings

Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean

@@ -3,8 +3,8 @@ Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.LinearAlgebra.Multilinear.Basic
 import Mathlib.Topology.Algebra.Module.LinearMapPiProd
+import Mathlib.LinearAlgebra.Multilinear.Basic
 
 /-!
 # Continuous multilinear maps