diff --git a/Mathlib.lean b/Mathlib.lean
index 30fd99db2bd0da..652ab69927fe78 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,9 @@ 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.Basis
+import Mathlib.LinearAlgebra.TensorProduct.DirectLimit
 import Mathlib.LinearAlgebra.TensorProduct.Graded.External
 import Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
 import Mathlib.LinearAlgebra.TensorProduct.Matrix
@@ -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.TensorProductBasis
 import Mathlib.LinearAlgebra.Trace
 import Mathlib.LinearAlgebra.UnitaryGroup
 import Mathlib.LinearAlgebra.Vandermonde
@@ -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
diff --git a/Mathlib/Algebra/Algebra/Bilinear.lean b/Mathlib/Algebra/Algebra/Bilinear.lean
index cd3d6e7f5d699f..c8356dbbba9e7b 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/AlgebraCat/Monoidal.lean b/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
index 56103d1581601d..21069120f5f21c 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 6c3e1d14dc9534..c491664f342a79 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/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
index 88549728edaedf..67a4b7948e7854 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/Algebra/Category/Ring/Constructions.lean b/Mathlib/Algebra/Category/Ring/Constructions.lean
index 111c86a2e54453..be1310396166c4 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 d80e71891761c1..6d880df5c82c3b 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 1cec22b7c7f1f5..446452ed6f8fbd 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 d26af1e27d152f..b3984287773845 100644
--- a/Mathlib/Data/Matrix/Kronecker.lean
+++ b/Mathlib/Data/Matrix/Kronecker.lean
@@ -7,8 +7,8 @@ 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.RingTheory.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
+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 071f3acb085c83..9df83b0beaafd3 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 ab3898cd51e2fe..f9abf873400026 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/DirectSum/TensorProduct.lean b/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
index f44c3f769bcbd5..9388b64430dfb4 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/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean
index 23401f67c0d9f7..638132f25aef47 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/FreeModule/Basic.lean b/Mathlib/LinearAlgebra/FreeModule/Basic.lean
index d7affa8128fc3e..d9a9af982cdf81 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/Multilinear/TensorProduct.lean b/Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean
index 73ffae3c1e84bd..9e9a07f3362c1c 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.lean b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
similarity index 100%
rename from Mathlib/LinearAlgebra/TensorProduct.lean
rename to Mathlib/LinearAlgebra/TensorProduct/Basic.lean
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
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
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean b/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
index b1066fe2e12e68..e7d3d749efea4e 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/Matrix.lean b/Mathlib/LinearAlgebra/TensorProduct/Matrix.lean
index 5650bfa844dfd2..bc43c305d15e76 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"
 
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Opposite.lean b/Mathlib/LinearAlgebra/TensorProduct/Opposite.lean
index 75f65e40559b0b..0d36c5ea524989 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/Prod.lean b/Mathlib/LinearAlgebra/TensorProduct/Prod.lean
index 9bd00033ebb036..458f1d4c8d1cea 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/RightExactness.lean b/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
index e755520bcbcee3..898d105b149189 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/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean
index 81f7726e0416b3..90c0677e95f5d9 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/RepresentationTheory/Basic.lean b/Mathlib/RepresentationTheory/Basic.lean
index 77461063254b62..5a6d65337dc053 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 239264bbaabfd4..9899f4a97127ec 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/Coalgebra.lean b/Mathlib/RingTheory/Coalgebra.lean
index 155c0d5edad7b6..5f6bea984287e6 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
diff --git a/Mathlib/RingTheory/IntegralClosure.lean b/Mathlib/RingTheory/IntegralClosure.lean
index d64592ab50ed12..b2a464047982a2 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 e58c642d2e38ba..34ddf305c6fe6e 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 78d07ee48a3fca..b36165d18ff671 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/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
diff --git a/test/instance_diamonds.lean b/test/instance_diamonds.lean
index b3d427ac9c23d6..7f6064fceb39f7 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 -/