refactor(LinearAlgebra/TensorProduct): split large file (#34798)

Split > 1500-line file `Mathlib/LinearAlgebra/TensorProduct/Basic.lean` into 3 more manageable chunks:

- `Defs.lean`: definition of `M ⊗ N` as a quotient of `FreeAddMonoid (M × N)` (500 lines)
- `Basic.lean`: universal property of `M ⊗ N`, lifting bilinear maps `M → N → P` to linear maps `M ⊗ N → P` (380 lines)
- `Map.lean`: linear maps `M ⊗ N → M' ⊗ N'` induced by maps `M → M'` and `N → N'` (and one-sided versions of that) (750 lines)

Author: loefflerd

Mathlib.lean

@@ -4886,11 +4886,13 @@ public import Mathlib.LinearAlgebra.TensorPower.Symmetric
 public import Mathlib.LinearAlgebra.TensorProduct.Associator
 public import Mathlib.LinearAlgebra.TensorProduct.Basic
 public import Mathlib.LinearAlgebra.TensorProduct.Basis
+public import Mathlib.LinearAlgebra.TensorProduct.Defs
 public import Mathlib.LinearAlgebra.TensorProduct.DirectLimit
 public import Mathlib.LinearAlgebra.TensorProduct.Finiteness
 public import Mathlib.LinearAlgebra.TensorProduct.Free
 public import Mathlib.LinearAlgebra.TensorProduct.Graded.External
 public import Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
+public import Mathlib.LinearAlgebra.TensorProduct.Map
 public import Mathlib.LinearAlgebra.TensorProduct.Matrix
 public import Mathlib.LinearAlgebra.TensorProduct.Opposite
 public import Mathlib.LinearAlgebra.TensorProduct.Pi

Mathlib/Algebra/Algebra/Bilinear.lean

@@ -6,7 +6,7 @@ Authors: Kenny Lau, Yury Kudryashov
 module
 
 public import Mathlib.Algebra.Algebra.NonUnitalHom
-public import Mathlib.LinearAlgebra.TensorProduct.Basic
+public import Mathlib.LinearAlgebra.TensorProduct.Map
 
 /-!
 # Facts about algebras involving bilinear maps and tensor products

Mathlib/Algebra/Star/TensorProduct.lean

@@ -6,7 +6,7 @@ Authors: Monica Omar
 module
 
 public import Mathlib.Algebra.Star.Module
-public import Mathlib.LinearAlgebra.TensorProduct.Basic
+public import Mathlib.LinearAlgebra.TensorProduct.Map
 
 /-!
 # The star structure on tensor products

Mathlib/Analysis/InnerProductSpace/TensorProduct.lean

@@ -6,9 +6,6 @@ Authors: Monica Omar
 module
 
 public import Mathlib.Analysis.InnerProductSpace.Adjoint
-public import Mathlib.Analysis.InnerProductSpace.LinearMap
-public import Mathlib.Analysis.InnerProductSpace.PiL2
-public import Mathlib.LinearAlgebra.TensorProduct.Basic
 public import Mathlib.LinearAlgebra.TensorProduct.Finiteness
 public import Mathlib.RingTheory.TensorProduct.Finite
 

Mathlib/Geometry/Convex/Cone/TensorProduct.lean

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Geometry.Convex.Cone.Dual
 public import Mathlib.LinearAlgebra.Dual.Lemmas
-public import Mathlib.LinearAlgebra.TensorProduct.Basic
+public import Mathlib.LinearAlgebra.TensorProduct.Defs
 
 /-!
 # Tensor products of cones

Mathlib/LinearAlgebra/Matrix/Kronecker.lean

@@ -5,14 +5,10 @@ Authors: Filippo A. E. Nuccio, Eric Wieser
 -/
 module
 
-public import Mathlib.Data.Matrix.Basic
-public import Mathlib.Data.Matrix.Block
+public import Mathlib.GroupTheory.GroupAction.Ring
 public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
 public import Mathlib.LinearAlgebra.Matrix.Trace
-public import Mathlib.LinearAlgebra.TensorProduct.Basic
-public import Mathlib.LinearAlgebra.TensorProduct.Associator
 public import Mathlib.RingTheory.TensorProduct.Basic
-public import Mathlib.GroupTheory.GroupAction.Ring
 
 /-!
 # Kronecker product of matrices

Mathlib/LinearAlgebra/TensorProduct/Associator.lean

@@ -6,7 +6,7 @@ Authors: Kenny Lau, Mario Carneiro
 module
 
 public import Mathlib.Algebra.Algebra.Hom
-public import Mathlib.LinearAlgebra.TensorProduct.Basic
+public import Mathlib.LinearAlgebra.TensorProduct.Map
 
 /-!
 # Associators and unitors for tensor products of modules over a commutative ring.