From 3844ac4a15892e798c8d7a08577fe4b9d398719f Mon Sep 17 00:00:00 2001
From: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Date: Sun, 10 Mar 2024 20:24:09 +0100
Subject: [PATCH 1/9] Mv DirectLimitAndTensorProduct to another folder and
 rename

---
 .../TensorProduct/DirectLimit.lean}                               | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename Mathlib/{Algebra/Module/DirectLimitAndTensorProduct.lean => LinearAlgebra/TensorProduct/DirectLimit.lean} (100%)

diff --git a/Mathlib/Algebra/Module/DirectLimitAndTensorProduct.lean b/Mathlib/LinearAlgebra/TensorProduct/DirectLimit.lean
similarity index 100%
rename from Mathlib/Algebra/Module/DirectLimitAndTensorProduct.lean
rename to Mathlib/LinearAlgebra/TensorProduct/DirectLimit.lean

From 256e55ede8bd0b444681d6e53cf51154691b5150 Mon Sep 17 00:00:00 2001
From: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Date: Sun, 10 Mar 2024 20:24:36 +0100
Subject: [PATCH 2/9] Mv TensorProduct.lean to TensorProduct/Basic.lean

---
 .../{TensorProduct.lean => TensorProduct/Basic.lean}              | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename Mathlib/LinearAlgebra/{TensorProduct.lean => TensorProduct/Basic.lean} (100%)

diff --git a/Mathlib/LinearAlgebra/TensorProduct.lean b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
similarity index 100%
rename from Mathlib/LinearAlgebra/TensorProduct.lean
rename to Mathlib/LinearAlgebra/TensorProduct/Basic.lean

From 06e4d011567e17bacd82e866b165ab42705305bd Mon Sep 17 00:00:00 2001
From: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Date: Sun, 10 Mar 2024 20:24:54 +0100
Subject: [PATCH 3/9] mv TensorProductBasis.lean to TensorProduct/Basis.lean

---
 .../{TensorProductBasis.lean => TensorProduct/Basis.lean}         | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename Mathlib/LinearAlgebra/{TensorProductBasis.lean => TensorProduct/Basis.lean} (100%)

diff --git a/Mathlib/LinearAlgebra/TensorProductBasis.lean b/Mathlib/LinearAlgebra/TensorProduct/Basis.lean
similarity index 100%
rename from Mathlib/LinearAlgebra/TensorProductBasis.lean
rename to Mathlib/LinearAlgebra/TensorProduct/Basis.lean

From 9051c25e91bafa9559cd0b68e16a05fcc56c3bc9 Mon Sep 17 00:00:00 2001
From: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Date: Sun, 10 Mar 2024 20:27:42 +0100
Subject: [PATCH 4/9] mv RingTheory/TensorProduct.lean to
 RingTheory/TensorProduct/Basic.lean

---
 .../RingTheory/{TensorProduct.lean => TensorProduct/Basic.lean}   | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename Mathlib/RingTheory/{TensorProduct.lean => TensorProduct/Basic.lean} (100%)

diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct/Basic.lean
similarity index 100%
rename from Mathlib/RingTheory/TensorProduct.lean
rename to Mathlib/RingTheory/TensorProduct/Basic.lean

From 400b21a84d0b21339375cff7c9173424876b8277 Mon Sep 17 00:00:00 2001
From: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Date: Sun, 10 Mar 2024 20:35:57 +0100
Subject: [PATCH 5/9] update Mathlib.lean

---
 Mathlib.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 30fd99db2bd0d..dabab3c816650 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -333,7 +333,6 @@ import Mathlib.Algebra.Module.BigOperators
 import Mathlib.Algebra.Module.Bimodule
 import Mathlib.Algebra.Module.CharacterModule
 import Mathlib.Algebra.Module.DedekindDomain
-import Mathlib.Algebra.Module.DirectLimitAndTensorProduct
 import Mathlib.Algebra.Module.Equiv
 import Mathlib.Algebra.Module.GradedModule
 import Mathlib.Algebra.Module.Hom
@@ -2652,7 +2651,8 @@ import Mathlib.LinearAlgebra.TensorAlgebra.Basis
 import Mathlib.LinearAlgebra.TensorAlgebra.Grading
 import Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
 import Mathlib.LinearAlgebra.TensorPower
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
+import Mathlib.LinearAlgebra.TensorProduct.DirectLimit
 import Mathlib.LinearAlgebra.TensorProduct.Graded.External
 import Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
 import Mathlib.LinearAlgebra.TensorProduct.Matrix
@@ -3404,7 +3404,7 @@ import Mathlib.RingTheory.Subring.Units
 import Mathlib.RingTheory.Subsemiring.Basic
 import Mathlib.RingTheory.Subsemiring.Order
 import Mathlib.RingTheory.Subsemiring.Pointwise
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.RingTheory.Trace
 import Mathlib.RingTheory.UniqueFactorizationDomain
 import Mathlib.RingTheory.Valuation.Basic

From 74d63a1af13a9110657af52de4ec7545995949e2 Mon Sep 17 00:00:00 2001
From: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Date: Sun, 10 Mar 2024 20:40:42 +0100
Subject: [PATCH 6/9] update import line in files importing
 Mathlib/Algebra/TensorProduct

---
 Mathlib/Algebra/Algebra/Bilinear.lean                  | 2 +-
 Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean | 2 +-
 Mathlib/Data/Matrix/Kronecker.lean                     | 2 +-
 Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean     | 2 +-
 Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean   | 2 +-
 Mathlib/LinearAlgebra/TensorProduct/Prod.lean          | 2 +-
 Mathlib/LinearAlgebra/TensorProduct/Tower.lean         | 2 +-
 Mathlib/RingTheory/Coalgebra.lean                      | 2 +-
 8 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Algebra/Algebra/Bilinear.lean b/Mathlib/Algebra/Algebra/Bilinear.lean
index cd3d6e7f5d699..c8356dbbba9e7 100644
--- a/Mathlib/Algebra/Algebra/Bilinear.lean
+++ b/Mathlib/Algebra/Algebra/Bilinear.lean
@@ -6,7 +6,7 @@ Authors: Kenny Lau, Yury Kudryashov
 import Mathlib.Algebra.Algebra.Basic
 import Mathlib.Algebra.Algebra.NonUnitalHom
 import Mathlib.Algebra.GroupPower.IterateHom
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 
 #align_import algebra.algebra.bilinear from "leanprover-community/mathlib"@"657df4339ae6ceada048c8a2980fb10e393143ec"
 
diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
index 88549728edaed..67a4b7948e785 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Scott Morrison, Jakob von Raumer
 -/
 import Mathlib.Algebra.Category.ModuleCat.Basic
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 import Mathlib.CategoryTheory.Monoidal.Linear
 
 #align_import algebra.category.Module.monoidal.basic from "leanprover-community/mathlib"@"74403a3b2551b0970855e14ef5e8fd0d6af1bfc2"
diff --git a/Mathlib/Data/Matrix/Kronecker.lean b/Mathlib/Data/Matrix/Kronecker.lean
index d26af1e27d152..a69fbfbf0fe7a 100644
--- a/Mathlib/Data/Matrix/Kronecker.lean
+++ b/Mathlib/Data/Matrix/Kronecker.lean
@@ -7,7 +7,7 @@ import Mathlib.Data.Matrix.Basic
 import Mathlib.Data.Matrix.Block
 import Mathlib.LinearAlgebra.Matrix.Determinant
 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 import Mathlib.RingTheory.TensorProduct
 
 #align_import data.matrix.kronecker from "leanprover-community/mathlib"@"3e068ece210655b7b9a9477c3aff38a492400aa1"
diff --git a/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean b/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
index f44c3f769bcbd..9388b64430dfb 100644
--- a/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
+++ b/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Mario Carneiro, Eric Wieser
 -/
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 import Mathlib.Algebra.DirectSum.Module
 
 #align_import linear_algebra.direct_sum.tensor_product from "leanprover-community/mathlib"@"9b9d125b7be0930f564a68f1d73ace10cf46064d"
diff --git a/Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean b/Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean
index 73ffae3c1e84b..9e9a07f3362c1 100644
--- a/Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean
+++ b/Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.LinearAlgebra.Multilinear.Basic
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 
 #align_import linear_algebra.multilinear.tensor_product from "leanprover-community/mathlib"@"ce11c3c2a285bbe6937e26d9792fda4e51f3fe1a"
 
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Prod.lean b/Mathlib/LinearAlgebra/TensorProduct/Prod.lean
index 9bd00033ebb03..458f1d4c8d1ce 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Prod.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Prod.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 import Mathlib.LinearAlgebra.Prod
 
 /-!
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean
index 81f7726e0416b..90c0677e95f5d 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean
@@ -5,7 +5,7 @@ Authors: Scott Morrison, Johan Commelin, Eric Wieser
 -/
 import Mathlib.Algebra.Algebra.Tower
 import Mathlib.LinearAlgebra.Basic
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 
 #align_import ring_theory.tensor_product from "leanprover-community/mathlib"@"88fcdc3da43943f5b01925deddaa5bf0c0e85e4e"
 
diff --git a/Mathlib/RingTheory/Coalgebra.lean b/Mathlib/RingTheory/Coalgebra.lean
index 155c0d5edad7b..5f6bea984287e 100644
--- a/Mathlib/RingTheory/Coalgebra.lean
+++ b/Mathlib/RingTheory/Coalgebra.lean
@@ -5,7 +5,7 @@ Authors: Ali Ramsey, Eric Wieser
 -/
 import Mathlib.LinearAlgebra.Finsupp
 import Mathlib.LinearAlgebra.Prod
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 
 /-!
 # Coalgebras

From c6324858ef417023e019fe703552687bc10eac74 Mon Sep 17 00:00:00 2001
From: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Date: Sun, 10 Mar 2024 20:41:59 +0100
Subject: [PATCH 7/9] update import line in files importing
 Mathlib/RingTheory/TensorProduct

---
 Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean        | 2 +-
 Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean    | 2 +-
 Mathlib/Algebra/Category/Ring/Constructions.lean         | 2 +-
 Mathlib/Algebra/Lie/BaseChange.lean                      | 2 +-
 Mathlib/Algebra/Module/Bimodule.lean                     | 2 +-
 Mathlib/Data/Matrix/Kronecker.lean                       | 2 +-
 Mathlib/FieldTheory/Adjoin.lean                          | 2 +-
 Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean    | 2 +-
 Mathlib/LinearAlgebra/Dual.lean                          | 2 +-
 Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean | 2 +-
 Mathlib/LinearAlgebra/TensorProduct/Opposite.lean        | 2 +-
 Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean  | 2 +-
 Mathlib/RepresentationTheory/Basic.lean                  | 2 +-
 Mathlib/RingTheory/Bialgebra.lean                        | 2 +-
 Mathlib/RingTheory/IntegralClosure.lean                  | 2 +-
 Mathlib/RingTheory/IsTensorProduct.lean                  | 2 +-
 Mathlib/RingTheory/MatrixAlgebra.lean                    | 2 +-
 test/instance_diamonds.lean                              | 2 +-
 18 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean b/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
index 56103d1581601..21069120f5f21 100644
--- a/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
+++ b/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
@@ -6,7 +6,7 @@ Authors: Eric Wieser
 import Mathlib.CategoryTheory.Monoidal.Transport
 import Mathlib.Algebra.Category.AlgebraCat.Basic
 import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 /-!
 # The monoidal category structure on R-algebras
diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
index 6c3e1d14dc953..c491664f342a7 100644
--- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang
 -/
 import Mathlib.Algebra.Category.ModuleCat.EpiMono
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import algebra.category.Module.change_of_rings from "leanprover-community/mathlib"@"56b71f0b55c03f70332b862e65c3aa1aa1249ca1"
 
diff --git a/Mathlib/Algebra/Category/Ring/Constructions.lean b/Mathlib/Algebra/Category/Ring/Constructions.lean
index 111c86a2e5445..be1310396166c 100644
--- a/Mathlib/Algebra/Category/Ring/Constructions.lean
+++ b/Mathlib/Algebra/Category/Ring/Constructions.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.Algebra.Category.Ring.Limits
 import Mathlib.Algebra.Category.Ring.Instances
 import Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
diff --git a/Mathlib/Algebra/Lie/BaseChange.lean b/Mathlib/Algebra/Lie/BaseChange.lean
index d80e71891761c..6d880df5c82c3 100644
--- a/Mathlib/Algebra/Lie/BaseChange.lean
+++ b/Mathlib/Algebra/Lie/BaseChange.lean
@@ -6,7 +6,7 @@ Authors: Oliver Nash
 import Mathlib.Algebra.Algebra.RestrictScalars
 import Mathlib.Algebra.Lie.TensorProduct
 import Mathlib.LinearAlgebra.TensorProduct.Tower
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import algebra.lie.base_change from "leanprover-community/mathlib"@"9264b15ee696b7ca83f13c8ad67c83d6eb70b730"
 
diff --git a/Mathlib/Algebra/Module/Bimodule.lean b/Mathlib/Algebra/Module/Bimodule.lean
index 1cec22b7c7f1f..446452ed6f8fb 100644
--- a/Mathlib/Algebra/Module/Bimodule.lean
+++ b/Mathlib/Algebra/Module/Bimodule.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.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import algebra.module.bimodule from "leanprover-community/mathlib"@"58cef51f7a819e7227224461e392dee423302f2d"
 
diff --git a/Mathlib/Data/Matrix/Kronecker.lean b/Mathlib/Data/Matrix/Kronecker.lean
index a69fbfbf0fe7a..b398428777384 100644
--- a/Mathlib/Data/Matrix/Kronecker.lean
+++ b/Mathlib/Data/Matrix/Kronecker.lean
@@ -8,7 +8,7 @@ import Mathlib.Data.Matrix.Block
 import Mathlib.LinearAlgebra.Matrix.Determinant
 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
 import Mathlib.LinearAlgebra.TensorProduct.Basic
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import data.matrix.kronecker from "leanprover-community/mathlib"@"3e068ece210655b7b9a9477c3aff38a492400aa1"
 
diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean
index 071f3acb085c8..9df83b0beaafd 100644
--- a/Mathlib/FieldTheory/Adjoin.lean
+++ b/Mathlib/FieldTheory/Adjoin.lean
@@ -6,7 +6,7 @@ Authors: Thomas Browning, Patrick Lutz
 import Mathlib.FieldTheory.IntermediateField
 import Mathlib.FieldTheory.Separable
 import Mathlib.FieldTheory.SplittingField.IsSplittingField
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import field_theory.adjoin from "leanprover-community/mathlib"@"df76f43357840485b9d04ed5dee5ab115d420e87"
 
diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
index ab3898cd51e2f..f9abf87340002 100644
--- a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
+++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
@@ -6,7 +6,7 @@ Authors: Eric Wieser
 import Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
 import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
 import Mathlib.LinearAlgebra.TensorProduct.Opposite
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 /-!
 # The base change of a clifford algebra
diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean
index 23401f67c0d9f..638132f25aef4 100644
--- a/Mathlib/LinearAlgebra/Dual.lean
+++ b/Mathlib/LinearAlgebra/Dual.lean
@@ -9,7 +9,7 @@ import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
 import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 import Mathlib.LinearAlgebra.Projection
 import Mathlib.LinearAlgebra.SesquilinearForm
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import linear_algebra.dual from "leanprover-community/mathlib"@"b1c017582e9f18d8494e5c18602a8cb4a6f843ac"
 
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean b/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
index b1066fe2e12e6..e7d3d749efea4 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
@@ -5,7 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.Data.Int.Order.Units
 import Mathlib.Data.ZMod.IntUnitsPower
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.LinearAlgebra.DirectSum.TensorProduct
 import Mathlib.Algebra.DirectSum.Algebra
 
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Opposite.lean b/Mathlib/LinearAlgebra/TensorProduct/Opposite.lean
index 75f65e40559b0..0d36c5ea52498 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Opposite.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Opposite.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.Algebra.Algebra.Opposite
 
 /-! # `MulOpposite` distributes over `⊗`
diff --git a/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean b/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
index e755520bcbcee..898d105b14918 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
@@ -5,7 +5,7 @@ Authors: Antoine Chambetr-Loir
 -/
 
 import Mathlib.Algebra.Exact
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 /-! # Right-exactness properties of tensor product
 
diff --git a/Mathlib/RepresentationTheory/Basic.lean b/Mathlib/RepresentationTheory/Basic.lean
index 77461063254b6..5a6d65337dc05 100644
--- a/Mathlib/RepresentationTheory/Basic.lean
+++ b/Mathlib/RepresentationTheory/Basic.lean
@@ -9,7 +9,7 @@ import Mathlib.Algebra.Module.LinearMap.Basic
 import Mathlib.Algebra.MonoidAlgebra.Basic
 import Mathlib.LinearAlgebra.Dual
 import Mathlib.LinearAlgebra.Contraction
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import representation_theory.basic from "leanprover-community/mathlib"@"c04bc6e93e23aa0182aba53661a2211e80b6feac"
 
diff --git a/Mathlib/RingTheory/Bialgebra.lean b/Mathlib/RingTheory/Bialgebra.lean
index 239264bbaabfd..9899f4a97127e 100644
--- a/Mathlib/RingTheory/Bialgebra.lean
+++ b/Mathlib/RingTheory/Bialgebra.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ali Ramsey, Kevin Buzzard
 -/
 import Mathlib.RingTheory.Coalgebra
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 /-!
 # Bialgebras
diff --git a/Mathlib/RingTheory/IntegralClosure.lean b/Mathlib/RingTheory/IntegralClosure.lean
index d64592ab50ed1..b2a464047982a 100644
--- a/Mathlib/RingTheory/IntegralClosure.lean
+++ b/Mathlib/RingTheory/IntegralClosure.lean
@@ -10,7 +10,7 @@ import Mathlib.RingTheory.Adjoin.FG
 import Mathlib.RingTheory.FiniteType
 import Mathlib.RingTheory.Polynomial.ScaleRoots
 import Mathlib.RingTheory.Polynomial.Tower
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import ring_theory.integral_closure from "leanprover-community/mathlib"@"641b6a82006416ec431b2987b354af9311fed4f2"
 
diff --git a/Mathlib/RingTheory/IsTensorProduct.lean b/Mathlib/RingTheory/IsTensorProduct.lean
index e58c642d2e38b..34ddf305c6fe6 100644
--- a/Mathlib/RingTheory/IsTensorProduct.lean
+++ b/Mathlib/RingTheory/IsTensorProduct.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.Algebra.Module.ULift
 
 #align_import ring_theory.is_tensor_product from "leanprover-community/mathlib"@"c4926d76bb9c5a4a62ed2f03d998081786132105"
diff --git a/Mathlib/RingTheory/MatrixAlgebra.lean b/Mathlib/RingTheory/MatrixAlgebra.lean
index 78d07ee48a3fc..b36165d18ff67 100644
--- a/Mathlib/RingTheory/MatrixAlgebra.lean
+++ b/Mathlib/RingTheory/MatrixAlgebra.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Eric Wieser
 -/
 import Mathlib.Data.Matrix.Basis
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import ring_theory.matrix_algebra from "leanprover-community/mathlib"@"6c351a8fb9b06e5a542fdf427bfb9f46724f9453"
 
diff --git a/test/instance_diamonds.lean b/test/instance_diamonds.lean
index b3d427ac9c23d..7f6064fceb39f 100644
--- a/test/instance_diamonds.lean
+++ b/test/instance_diamonds.lean
@@ -10,7 +10,7 @@ import Mathlib.GroupTheory.GroupAction.Units
 import Mathlib.Data.Complex.Module
 import Mathlib.RingTheory.Algebraic
 import Mathlib.Data.ZMod.Basic
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 /-! # Tests that instances do not form diamonds -/
 

From 417a468ed9a7e635f932a91df07aa6452bad5c40 Mon Sep 17 00:00:00 2001
From: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Date: Sun, 10 Mar 2024 22:53:29 +0100
Subject: [PATCH 8/9] Update import line about
 LinearAlgebra/TensorProduct/Basis

---
 Mathlib.lean                                    | 2 +-
 Mathlib/LinearAlgebra/FreeModule/Basic.lean     | 2 +-
 Mathlib/LinearAlgebra/TensorProduct/Matrix.lean | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index dabab3c816650..7824841f62e1c 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2660,7 +2660,7 @@ import Mathlib.LinearAlgebra.TensorProduct.Opposite
 import Mathlib.LinearAlgebra.TensorProduct.Prod
 import Mathlib.LinearAlgebra.TensorProduct.RightExactness
 import Mathlib.LinearAlgebra.TensorProduct.Tower
-import Mathlib.LinearAlgebra.TensorProductBasis
+import Mathlib.LinearAlgebra.TensorProduct.Basis
 import Mathlib.LinearAlgebra.Trace
 import Mathlib.LinearAlgebra.UnitaryGroup
 import Mathlib.LinearAlgebra.Vandermonde
diff --git a/Mathlib/LinearAlgebra/FreeModule/Basic.lean b/Mathlib/LinearAlgebra/FreeModule/Basic.lean
index d7affa8128fc3..d9a9af982cdf8 100644
--- a/Mathlib/LinearAlgebra/FreeModule/Basic.lean
+++ b/Mathlib/LinearAlgebra/FreeModule/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 -/
 import Mathlib.Data.Finsupp.Fintype
-import Mathlib.LinearAlgebra.TensorProductBasis
+import Mathlib.LinearAlgebra.TensorProduct.Basis
 
 #align_import linear_algebra.free_module.basic from "leanprover-community/mathlib"@"4e7e7009099d4a88a750de710909b95487bf0124"
 
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Matrix.lean b/Mathlib/LinearAlgebra/TensorProduct/Matrix.lean
index 5650bfa844dfd..bc43c305d15e7 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Matrix.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Matrix.lean
@@ -5,7 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.Data.Matrix.Kronecker
 import Mathlib.LinearAlgebra.Matrix.ToLin
-import Mathlib.LinearAlgebra.TensorProductBasis
+import Mathlib.LinearAlgebra.TensorProduct.Basis
 
 #align_import linear_algebra.tensor_product.matrix from "leanprover-community/mathlib"@"f784cc6142443d9ee623a20788c282112c322081"
 

From 7c1dd7c36be797c2f1c7ff68a537fd2af8826b6f Mon Sep 17 00:00:00 2001
From: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Date: Sun, 10 Mar 2024 22:56:15 +0100
Subject: [PATCH 9/9] update Mathlib.lean

---
 Mathlib.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 7824841f62e1c..652ab69927fe7 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2652,6 +2652,7 @@ import Mathlib.LinearAlgebra.TensorAlgebra.Grading
 import Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
 import Mathlib.LinearAlgebra.TensorPower
 import Mathlib.LinearAlgebra.TensorProduct.Basic
+import Mathlib.LinearAlgebra.TensorProduct.Basis
 import Mathlib.LinearAlgebra.TensorProduct.DirectLimit
 import Mathlib.LinearAlgebra.TensorProduct.Graded.External
 import Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
@@ -2660,7 +2661,6 @@ import Mathlib.LinearAlgebra.TensorProduct.Opposite
 import Mathlib.LinearAlgebra.TensorProduct.Prod
 import Mathlib.LinearAlgebra.TensorProduct.RightExactness
 import Mathlib.LinearAlgebra.TensorProduct.Tower
-import Mathlib.LinearAlgebra.TensorProduct.Basis
 import Mathlib.LinearAlgebra.Trace
 import Mathlib.LinearAlgebra.UnitaryGroup
 import Mathlib.LinearAlgebra.Vandermonde