From 5b04cac0e31a6953b498e5fe76337bd8d5d67d0d Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Mon, 22 Apr 2024 09:41:56 +0000
Subject: [PATCH] chore: redistribute a few results from
 Algebra.Module.Submodule.LinearMap (#12295)

These don't involve submodules at all.
---
 Mathlib/Algebra/Module/LinearMap/Basic.lean   | 25 ++++++++++++++++
 Mathlib/Algebra/Module/LinearMap/End.lean     |  4 +++
 .../Algebra/Module/Submodule/LinearMap.lean   | 29 -------------------
 3 files changed, 29 insertions(+), 29 deletions(-)

diff --git a/Mathlib/Algebra/Module/LinearMap/Basic.lean b/Mathlib/Algebra/Module/LinearMap/Basic.lean
index 4e05fa12b487d..9390e848e94f8 100644
--- a/Mathlib/Algebra/Module/LinearMap/Basic.lean
+++ b/Mathlib/Algebra/Module/LinearMap/Basic.lean
@@ -934,6 +934,15 @@ theorem default_def : (default : M →ₛₗ[σ₁₂] M₂) = 0 :=
   rfl
 #align linear_map.default_def LinearMap.default_def
 
+instance uniqueOfLeft [Subsingleton M] : Unique (M →ₛₗ[σ₁₂] M₂) :=
+  { inferInstanceAs (Inhabited (M →ₛₗ[σ₁₂] M₂)) with
+    uniq := fun f => ext fun x => by rw [Subsingleton.elim x 0, map_zero, map_zero] }
+#align linear_map.unique_of_left LinearMap.uniqueOfLeft
+
+instance uniqueOfRight [Subsingleton M₂] : Unique (M →ₛₗ[σ₁₂] M₂) :=
+  coe_injective.unique
+#align linear_map.unique_of_right LinearMap.uniqueOfRight
+
 /-- The sum of two linear maps is linear. -/
 instance : Add (M →ₛₗ[σ₁₂] M₂) :=
   ⟨fun f g ↦
@@ -1009,6 +1018,22 @@ instance addCommGroup : AddCommGroup (M →ₛₗ[σ₁₂] N₂) :=
   DFunLike.coe_injective.addCommGroup _ rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl)
     (fun _ _ ↦ rfl) fun _ _ ↦ rfl
 
+/-- Evaluation of a `σ₁₂`-linear map at a fixed `a`, as an `AddMonoidHom`. -/
+@[simps]
+def evalAddMonoidHom (a : M) : (M →ₛₗ[σ₁₂] M₂) →+ M₂ where
+  toFun f := f a
+  map_add' f g := LinearMap.add_apply f g a
+  map_zero' := rfl
+#align linear_map.eval_add_monoid_hom LinearMap.evalAddMonoidHom
+
+/-- `LinearMap.toAddMonoidHom` promoted to an `AddMonoidHom`. -/
+@[simps]
+def toAddMonoidHom' : (M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂ where
+  toFun := toAddMonoidHom
+  map_zero' := by ext; rfl
+  map_add' := by intros; ext; rfl
+#align linear_map.to_add_monoid_hom' LinearMap.toAddMonoidHom'
+
 end Arithmetic
 
 section Actions
diff --git a/Mathlib/Algebra/Module/LinearMap/End.lean b/Mathlib/Algebra/Module/LinearMap/End.lean
index 638116d04c5fe..d71f6d6988a66 100644
--- a/Mathlib/Algebra/Module/LinearMap/End.lean
+++ b/Mathlib/Algebra/Module/LinearMap/End.lean
@@ -67,6 +67,10 @@ theorem coe_one : ⇑(1 : Module.End R M) = _root_.id := rfl
 theorem coe_mul (f g : Module.End R M) : ⇑(f * g) = f ∘ g := rfl
 #align linear_map.coe_mul LinearMap.coe_mul
 
+instance _root_.Module.End.instNontrivial [Nontrivial M] : Nontrivial (Module.End R M) := by
+  obtain ⟨m, ne⟩ := exists_ne (0 : M)
+  exact nontrivial_of_ne 1 0 fun p => ne (LinearMap.congr_fun p m)
+
 instance _root_.Module.End.monoid : Monoid (Module.End R M) where
   mul := (· * ·)
   one := (1 : M →ₗ[R] M)
diff --git a/Mathlib/Algebra/Module/Submodule/LinearMap.lean b/Mathlib/Algebra/Module/Submodule/LinearMap.lean
index d66bcfa7259e2..4e91ea83b06e0 100644
--- a/Mathlib/Algebra/Module/Submodule/LinearMap.lean
+++ b/Mathlib/Algebra/Module/Submodule/LinearMap.lean
@@ -211,40 +211,11 @@ theorem restrict_eq_domRestrict_codRestrict {f : M →ₗ[R] M₁} {p : Submodul
   rfl
 #align linear_map.restrict_eq_dom_restrict_cod_restrict LinearMap.restrict_eq_domRestrict_codRestrict
 
-instance uniqueOfLeft [Subsingleton M] : Unique (M →ₛₗ[σ₁₂] M₂) :=
-  { inferInstanceAs (Inhabited (M →ₛₗ[σ₁₂] M₂)) with
-    uniq := fun f => ext fun x => by rw [Subsingleton.elim x 0, map_zero, map_zero] }
-#align linear_map.unique_of_left LinearMap.uniqueOfLeft
-
-instance uniqueOfRight [Subsingleton M₂] : Unique (M →ₛₗ[σ₁₂] M₂) :=
-  coe_injective.unique
-#align linear_map.unique_of_right LinearMap.uniqueOfRight
-
-/-- Evaluation of a `σ₁₂`-linear map at a fixed `a`, as an `AddMonoidHom`. -/
-@[simps]
-def evalAddMonoidHom (a : M) : (M →ₛₗ[σ₁₂] M₂) →+ M₂ where
-  toFun f := f a
-  map_add' f g := LinearMap.add_apply f g a
-  map_zero' := rfl
-#align linear_map.eval_add_monoid_hom LinearMap.evalAddMonoidHom
-
-/-- `LinearMap.toAddMonoidHom` promoted to an `AddMonoidHom`. -/
-@[simps]
-def toAddMonoidHom' : (M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂ where
-  toFun := toAddMonoidHom
-  map_zero' := by ext; rfl
-  map_add' := by intros; ext; rfl
-#align linear_map.to_add_monoid_hom' LinearMap.toAddMonoidHom'
-
 theorem sum_apply (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) (b : M) :
     (∑ d in t, f d) b = ∑ d in t, f d b :=
   _root_.map_sum ((AddMonoidHom.eval b).comp toAddMonoidHom') f _
 #align linear_map.sum_apply LinearMap.sum_apply
 
-instance [Nontrivial M] : Nontrivial (Module.End R M) := by
-  obtain ⟨m, ne⟩ := exists_ne (0 : M)
-  exact nontrivial_of_ne 1 0 fun p => ne (LinearMap.congr_fun p m)
-
 @[simp, norm_cast]
 theorem coeFn_sum {ι : Type*} (t : Finset ι) (f : ι → M →ₛₗ[σ₁₂] M₂) :
     ⇑(∑ i in t, f i) = ∑ i in t, (f i : M → M₂) :=