diff --git a/Mathlib.lean b/Mathlib.lean
index eb43971b28552..c41559b7da7c2 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -422,6 +422,7 @@ import Mathlib.Algebra.Module.Injective
 import Mathlib.Algebra.Module.LinearMap.Basic
 import Mathlib.Algebra.Module.LinearMap.End
 import Mathlib.Algebra.Module.LinearMap.Polynomial
+import Mathlib.Algebra.Module.LinearMap.Prod
 import Mathlib.Algebra.Module.LocalizedModule
 import Mathlib.Algebra.Module.LocalizedModuleIntegers
 import Mathlib.Algebra.Module.MinimalAxioms
diff --git a/Mathlib/Algebra/Module/LinearMap/Prod.lean b/Mathlib/Algebra/Module/LinearMap/Prod.lean
new file mode 100644
index 0000000000000..32c8b927045d1
--- /dev/null
+++ b/Mathlib/Algebra/Module/LinearMap/Prod.lean
@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2019 Alexander Bentkamp. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alexander Bentkamp
+-/
+
+import Mathlib.Algebra.Module.Prod
+import Mathlib.Algebra.Module.LinearMap.Basic
+import Mathlib.Tactic.Abel
+
+#align_import linear_algebra.basic from "leanprover-community/mathlib"@"9d684a893c52e1d6692a504a118bfccbae04feeb"
+
+/-!
+# Addition and subtraction are linear maps from the product space
+
+Note that these results use `IsLinearMap`, which is mostly discouraged.
+
+## Tags
+linear algebra, vector space, module
+
+-/
+
+variable {R : Type*} {M : Type*} [Semiring R]
+
+namespace IsLinearMap
+
+theorem isLinearMap_add [AddCommMonoid M] [Module R M] :
+    IsLinearMap R fun x : M × M => x.1 + x.2 := by
+  apply IsLinearMap.mk
+  · intro x y
+    simp only [Prod.fst_add, Prod.snd_add]
+    abel
+  · intro x y
+    simp [smul_add]
+#align is_linear_map.is_linear_map_add IsLinearMap.isLinearMap_add
+
+theorem isLinearMap_sub [AddCommGroup M] [Module R M] :
+    IsLinearMap R fun x : M × M => x.1 - x.2 := by
+  apply IsLinearMap.mk
+  · intro x y
+    -- porting note (#10745): was `simp [add_comm, add_left_comm, sub_eq_add_neg]`
+    rw [Prod.fst_add, Prod.snd_add]
+    abel
+  · intro x y
+    simp [smul_sub]
+#align is_linear_map.is_linear_map_sub IsLinearMap.isLinearMap_sub
+
+end IsLinearMap
diff --git a/Mathlib/Analysis/Convex/Star.lean b/Mathlib/Analysis/Convex/Star.lean
index 4e58cfe0d40f8..bfc135120bd7c 100644
--- a/Mathlib/Analysis/Convex/Star.lean
+++ b/Mathlib/Analysis/Convex/Star.lean
@@ -3,9 +3,9 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import Mathlib.Algebra.Module.LinearMap.Prod
 import Mathlib.Algebra.Order.Group.Instances
 import Mathlib.Analysis.Convex.Segment
-import Mathlib.LinearAlgebra.Basic
 import Mathlib.Tactic.GCongr
 
 #align_import analysis.convex.star from "leanprover-community/mathlib"@"9003f28797c0664a49e4179487267c494477d853"
diff --git a/Mathlib/LinearAlgebra/Basic.lean b/Mathlib/LinearAlgebra/Basic.lean
index 691715639d662..92f810f7a171a 100644
--- a/Mathlib/LinearAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/Basic.lean
@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Fréd
 -/
 import Mathlib.Algebra.BigOperators.Group.Finset
 import Mathlib.Algebra.Module.LinearMap.Basic
+import Mathlib.Algebra.Module.LinearMap.Prod
 import Mathlib.Algebra.Module.Prod
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Tactic.Abel
@@ -52,43 +53,6 @@ linear algebra, vector space, module
 
 -/
 
-open Function
-
-variable {R : Type*} {R₁ : Type*} {R₂ : Type*} {R₃ : Type*} {R₄ : Type*}
-variable {S : Type*}
-variable {K : Type*} {K₂ : Type*}
-variable {M : Type*} {M' : Type*} {M₁ : Type*} {M₂ : Type*} {M₃ : Type*} {M₄ : Type*}
-variable {N : Type*} {N₂ : Type*}
-variable {ι : Type*}
-variable {V : Type*} {V₂ : Type*}
-
-/-! ### Properties of linear maps -/
-
-namespace IsLinearMap
-
-theorem isLinearMap_add [Semiring R] [AddCommMonoid M] [Module R M] :
-    IsLinearMap R fun x : M × M => x.1 + x.2 := by
-  apply IsLinearMap.mk
-  · intro x y
-    simp only [Prod.fst_add, Prod.snd_add]
-    abel
-  · intro x y
-    simp [smul_add]
-#align is_linear_map.is_linear_map_add IsLinearMap.isLinearMap_add
-
-theorem isLinearMap_sub {R M : Type*} [Semiring R] [AddCommGroup M] [Module R M] :
-    IsLinearMap R fun x : M × M => x.1 - x.2 := by
-  apply IsLinearMap.mk
-  · intro x y
-    -- porting note (#10745): was `simp [add_comm, add_left_comm, sub_eq_add_neg]`
-    rw [Prod.fst_add, Prod.snd_add]
-    abel
-  · intro x y
-    simp [smul_sub]
-#align is_linear_map.is_linear_map_sub IsLinearMap.isLinearMap_sub
-
-end IsLinearMap
-
 #align linear_equiv.map_sum map_sumₓ
 #align linear_equiv.map_neg map_negₓ
 #align linear_equiv.map_sub map_subₓ