diff --git a/Mathlib.lean b/Mathlib.lean
index 490a65130c46c..93617be7efc12 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3233,8 +3233,9 @@ import Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric
 import Mathlib.LinearAlgebra.QuadraticForm.Real
 import Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
 import Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
-import Mathlib.LinearAlgebra.Quotient
-import Mathlib.LinearAlgebra.QuotientPi
+import Mathlib.LinearAlgebra.Quotient.Basic
+import Mathlib.LinearAlgebra.Quotient.Defs
+import Mathlib.LinearAlgebra.Quotient.Pi
 import Mathlib.LinearAlgebra.Ray
 import Mathlib.LinearAlgebra.Reflection
 import Mathlib.LinearAlgebra.RootSystem.Basic
diff --git a/Mathlib/Algebra/Category/ModuleCat/EpiMono.lean b/Mathlib/Algebra/Category/ModuleCat/EpiMono.lean
index 0a359d162c781..4ba5ef78289de 100644
--- a/Mathlib/Algebra/Category/ModuleCat/EpiMono.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/EpiMono.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.Algebra.Category.ModuleCat.Basic
 import Mathlib.CategoryTheory.ConcreteCategory.EpiMono
 
diff --git a/Mathlib/Algebra/DirectLimit.lean b/Mathlib/Algebra/DirectLimit.lean
index c5d8c1217f959..7788d99fae809 100644
--- a/Mathlib/Algebra/DirectLimit.lean
+++ b/Mathlib/Algebra/DirectLimit.lean
@@ -3,8 +3,9 @@ Copyright (c) 2019 Kenny Lau, Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Chris Hughes, Jujian Zhang
 -/
-import Mathlib.Data.Finset.Order
 import Mathlib.Algebra.DirectSum.Module
+import Mathlib.Data.Finset.Order
+import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.RingTheory.FreeCommRing
 import Mathlib.RingTheory.Ideal.Maps
 import Mathlib.RingTheory.Ideal.Quotient
diff --git a/Mathlib/Algebra/Exact.lean b/Mathlib/Algebra/Exact.lean
index e3eb8a8116504..23d6d705097ab 100644
--- a/Mathlib/Algebra/Exact.lean
+++ b/Mathlib/Algebra/Exact.lean
@@ -6,7 +6,7 @@ Authors: Antoine Chambert-Loir
 
 import Mathlib.Algebra.Module.Submodule.Range
 import Mathlib.LinearAlgebra.Prod
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 
 /-! # Exactness of a pair
 
diff --git a/Mathlib/Algebra/Module/Presentation/Basic.lean b/Mathlib/Algebra/Module/Presentation/Basic.lean
index 2c60a6a2c5ce4..df5cba4e2775d 100644
--- a/Mathlib/Algebra/Module/Presentation/Basic.lean
+++ b/Mathlib/Algebra/Module/Presentation/Basic.lean
@@ -6,7 +6,7 @@ Authors: Joël Riou
 import Mathlib.Algebra.Exact
 import Mathlib.Algebra.Module.Basic
 import Mathlib.LinearAlgebra.Finsupp
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 
 /-!
 # Presentations of modules
diff --git a/Mathlib/Algebra/Module/Submodule/Localization.lean b/Mathlib/Algebra/Module/Submodule/Localization.lean
index 3cc2176df7536..42dd4e3d8240d 100644
--- a/Mathlib/Algebra/Module/Submodule/Localization.lean
+++ b/Mathlib/Algebra/Module/Submodule/Localization.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.Algebra.Module.LocalizedModule
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.RingTheory.Localization.Module
 
 /-!
diff --git a/Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean b/Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean
index 054d145f3347d..81dfb10854f99 100644
--- a/Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean
+++ b/Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean
@@ -6,7 +6,7 @@ Authors: Anne Baanen
 import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
 import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
-import Mathlib.LinearAlgebra.QuotientPi
+import Mathlib.LinearAlgebra.Quotient.Pi
 import Mathlib.RingTheory.Ideal.Basis
 import Mathlib.LinearAlgebra.Dimension.Constructions
 
diff --git a/Mathlib/LinearAlgebra/Isomorphisms.lean b/Mathlib/LinearAlgebra/Isomorphisms.lean
index 3a94028500411..3dae0b8f30bfe 100644
--- a/Mathlib/LinearAlgebra/Isomorphisms.lean
+++ b/Mathlib/LinearAlgebra/Isomorphisms.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
 -/
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 
 /-!
 # Isomorphism theorems for modules.
diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean
index da597346dcca3..7a372e543c8fe 100644
--- a/Mathlib/LinearAlgebra/Projection.lean
+++ b/Mathlib/LinearAlgebra/Projection.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.LinearAlgebra.Prod
 
 /-!
diff --git a/Mathlib/LinearAlgebra/Quotient.lean b/Mathlib/LinearAlgebra/Quotient/Basic.lean
similarity index 66%
rename from Mathlib/LinearAlgebra/Quotient.lean
rename to Mathlib/LinearAlgebra/Quotient/Basic.lean
index d18b1003f7d28..0f5bd394978ce 100644
--- a/Mathlib/LinearAlgebra/Quotient.lean
+++ b/Mathlib/LinearAlgebra/Quotient/Basic.lean
@@ -3,10 +3,11 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
 -/
-import Mathlib.LinearAlgebra.Span
-import Mathlib.LinearAlgebra.Pi
 import Mathlib.Algebra.Module.Equiv.Basic
 import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.LinearAlgebra.Pi
+import Mathlib.LinearAlgebra.Quotient.Defs
+import Mathlib.LinearAlgebra.Span
 import Mathlib.SetTheory.Cardinal.Finite
 
 /-!
@@ -15,6 +16,14 @@ import Mathlib.SetTheory.Cardinal.Finite
 * If `p` is a submodule of `M`, `M ⧸ p` is the quotient of `M` with respect to `p`:
   that is, elements of `M` are identified if their difference is in `p`. This is itself a module.
 
+## Main definitions
+
+* `Submodule.Quotient.restrictScalarsEquiv`: The quotient of `P` as an `S`-submodule is the same
+  as the quotient of `P` as an `R`-submodule,
+* `Submodule.liftQ`: lift a map `M → M₂` to a map `M ⧸ p → M₂` if the kernel is contained in `p`
+* `Submodule.mapQ`: lift a map `M → M₂` to a map `M ⧸ p → M₂ ⧸ q` if the image of `p` is contained
+  in `q`
+
 -/
 
 -- For most of this file we work over a noncommutative ring
@@ -27,174 +36,11 @@ variable (p p' : Submodule R M)
 
 open LinearMap QuotientAddGroup
 
-/-- The equivalence relation associated to a submodule `p`, defined by `x ≈ y` iff `-x + y ∈ p`.
-
-Note this is equivalent to `y - x ∈ p`, but defined this way to be defeq to the `AddSubgroup`
-version, where commutativity can't be assumed. -/
-def quotientRel : Setoid M :=
-  QuotientAddGroup.leftRel p.toAddSubgroup
-
-theorem quotientRel_def {x y : M} : p.quotientRel x y ↔ x - y ∈ p :=
-  Iff.trans
-    (by
-      rw [leftRel_apply, sub_eq_add_neg, neg_add, neg_neg]
-      rfl)
-    neg_mem_iff
-
-@[deprecated (since := "2024-08-29")] alias quotientRel_r_def := quotientRel_def
-
-/-- The quotient of a module `M` by a submodule `p ⊆ M`. -/
-instance hasQuotient : HasQuotient M (Submodule R M) :=
-  ⟨fun p => Quotient (quotientRel p)⟩
-
 namespace Quotient
 
-/-- Map associating to an element of `M` the corresponding element of `M/p`,
-when `p` is a submodule of `M`. -/
-def mk {p : Submodule R M} : M → M ⧸ p :=
-  Quotient.mk''
-
-theorem mk'_eq_mk' {p : Submodule R M} (x : M) :
-    @Quotient.mk' _ (quotientRel p) x = mk x :=
-  rfl
-
-theorem mk''_eq_mk {p : Submodule R M} (x : M) : (Quotient.mk'' x : M ⧸ p) = mk x :=
-  rfl
-
-theorem quot_mk_eq_mk {p : Submodule R M} (x : M) : (Quot.mk _ x : M ⧸ p) = mk x :=
-  rfl
-
-protected theorem eq' {x y : M} : (mk x : M ⧸ p) = mk y ↔ -x + y ∈ p :=
-  QuotientAddGroup.eq
-
-protected theorem eq {x y : M} : (mk x : M ⧸ p) = mk y ↔ x - y ∈ p :=
-  (Submodule.Quotient.eq' p).trans (leftRel_apply.symm.trans p.quotientRel_def)
-
-instance : Zero (M ⧸ p) where
-  -- Use Quotient.mk'' instead of mk here because mk is not reducible.
-  -- This would lead to non-defeq diamonds.
-  -- See also the same comment at the One instance for Con.
-  zero := Quotient.mk'' 0
-
-instance : Inhabited (M ⧸ p) :=
-  ⟨0⟩
-
-@[simp]
-theorem mk_zero : mk 0 = (0 : M ⧸ p) :=
-  rfl
-
-@[simp]
-theorem mk_eq_zero : (mk x : M ⧸ p) = 0 ↔ x ∈ p := by simpa using (Quotient.eq' p : mk x = 0 ↔ _)
-
-instance addCommGroup : AddCommGroup (M ⧸ p) :=
-  QuotientAddGroup.Quotient.addCommGroup p.toAddSubgroup
-
-@[simp]
-theorem mk_add : (mk (x + y) : M ⧸ p) = mk x + mk y :=
-  rfl
-
-@[simp]
-theorem mk_neg : (mk (-x) : M ⧸ p) = -(mk x) :=
-  rfl
-
-@[simp]
-theorem mk_sub : (mk (x - y) : M ⧸ p) = mk x - mk y :=
-  rfl
-
-protected nonrec lemma «forall» {P : M ⧸ p → Prop} : (∀ a, P a) ↔ ∀ a, P (mk a) := Quotient.forall
-
-section SMul
-
-variable {S : Type*} [SMul S R] [SMul S M] [IsScalarTower S R M] (P : Submodule R M)
-
-instance instSMul' : SMul S (M ⧸ P) :=
-  ⟨fun a =>
-    Quotient.map' (a • ·) fun x y h =>
-      leftRel_apply.mpr <| by simpa using Submodule.smul_mem P (a • (1 : R)) (leftRel_apply.mp h)⟩
-
--- Porting note: should this be marked as a `@[default_instance]`?
-/-- Shortcut to help the elaborator in the common case. -/
-instance instSMul : SMul R (M ⧸ P) :=
-  Quotient.instSMul' P
-
-@[simp]
-theorem mk_smul (r : S) (x : M) : (mk (r • x) : M ⧸ p) = r • mk x :=
-  rfl
-
-instance smulCommClass (T : Type*) [SMul T R] [SMul T M] [IsScalarTower T R M]
-    [SMulCommClass S T M] : SMulCommClass S T (M ⧸ P) where
-  smul_comm _x _y := Quotient.ind' fun _z => congr_arg mk (smul_comm _ _ _)
-
-instance isScalarTower (T : Type*) [SMul T R] [SMul T M] [IsScalarTower T R M] [SMul S T]
-    [IsScalarTower S T M] : IsScalarTower S T (M ⧸ P) where
-  smul_assoc _x _y := Quotient.ind' fun _z => congr_arg mk (smul_assoc _ _ _)
-
-instance isCentralScalar [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M]
-    [IsCentralScalar S M] : IsCentralScalar S (M ⧸ P) where
-  op_smul_eq_smul _x := Quotient.ind' fun _z => congr_arg mk <| op_smul_eq_smul _ _
-
-end SMul
-
 section Module
 
-variable {S : Type*}
-
--- Performance of `Function.Surjective.mulAction` is worse since it has to unify data to apply
--- TODO: leanprover-community/mathlib4#7432
-instance mulAction' [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M]
-    (P : Submodule R M) : MulAction S (M ⧸ P) :=
-  { Function.Surjective.mulAction mk (surjective_quot_mk _) <| Submodule.Quotient.mk_smul P with
-    toSMul := instSMul' _ }
-
--- Porting note: should this be marked as a `@[default_instance]`?
-instance mulAction (P : Submodule R M) : MulAction R (M ⧸ P) :=
-  Quotient.mulAction' P
-
-instance smulZeroClass' [SMul S R] [SMulZeroClass S M] [IsScalarTower S R M] (P : Submodule R M) :
-    SMulZeroClass S (M ⧸ P) :=
-  ZeroHom.smulZeroClass ⟨mk, mk_zero _⟩ <| Submodule.Quotient.mk_smul P
-
--- Porting note: should this be marked as a `@[default_instance]`?
-instance smulZeroClass (P : Submodule R M) : SMulZeroClass R (M ⧸ P) :=
-  Quotient.smulZeroClass' P
-
--- Performance of `Function.Surjective.distribSMul` is worse since it has to unify data to apply
--- TODO: leanprover-community/mathlib4#7432
-instance distribSMul' [SMul S R] [DistribSMul S M] [IsScalarTower S R M] (P : Submodule R M) :
-    DistribSMul S (M ⧸ P) :=
-  { Function.Surjective.distribSMul {toFun := mk, map_zero' := rfl, map_add' := fun _ _ => rfl}
-    (surjective_quot_mk _) (Submodule.Quotient.mk_smul P) with
-    toSMulZeroClass := smulZeroClass' _ }
-
--- Porting note: should this be marked as a `@[default_instance]`?
-instance distribSMul (P : Submodule R M) : DistribSMul R (M ⧸ P) :=
-  Quotient.distribSMul' P
-
--- Performance of `Function.Surjective.distribMulAction` is worse since it has to unify data
--- TODO: leanprover-community/mathlib4#7432
-instance distribMulAction' [Monoid S] [SMul S R] [DistribMulAction S M] [IsScalarTower S R M]
-    (P : Submodule R M) : DistribMulAction S (M ⧸ P) :=
-  { Function.Surjective.distribMulAction {toFun := mk, map_zero' := rfl, map_add' := fun _ _ => rfl}
-    (surjective_quot_mk _) (Submodule.Quotient.mk_smul P) with
-    toMulAction := mulAction' _ }
-
--- Porting note: should this be marked as a `@[default_instance]`?
-instance distribMulAction (P : Submodule R M) : DistribMulAction R (M ⧸ P) :=
-  Quotient.distribMulAction' P
-
--- Performance of `Function.Surjective.module` is worse since it has to unify data to apply
--- TODO: leanprover-community/mathlib4#7432
-instance module' [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) :
-    Module S (M ⧸ P) :=
-  { Function.Surjective.module _ {toFun := mk, map_zero' := by rfl, map_add' := fun _ _ => by rfl}
-    (surjective_quot_mk _) (Submodule.Quotient.mk_smul P) with
-    toDistribMulAction := distribMulAction' _ }
-
--- Porting note: should this be marked as a `@[default_instance]`?
-instance module (P : Submodule R M) : Module R (M ⧸ P) :=
-  Quotient.module' P
-
-variable (S)
+variable (S : Type*)
 
 /-- The quotient of `P` as an `S`-submodule is the same as the quotient of `P` as an `R`-submodule,
 where `P : Submodule R M`.
@@ -219,10 +65,6 @@ theorem restrictScalarsEquiv_symm_mk [Ring S] [SMul S R] [Module S M] [IsScalarT
 
 end Module
 
-theorem mk_surjective : Function.Surjective (@mk _ _ _ _ _ p) := by
-  rintro ⟨x⟩
-  exact ⟨x, rfl⟩
-
 theorem nontrivial_of_lt_top (h : p < ⊤) : Nontrivial (M ⧸ p) := by
   obtain ⟨x, _, not_mem_s⟩ := SetLike.exists_of_lt h
   refine ⟨⟨mk x, 0, ?_⟩⟩
@@ -270,23 +112,6 @@ section
 
 variable {M₂ : Type*} [AddCommGroup M₂] [Module R M₂]
 
-theorem quot_hom_ext (f g : (M ⧸ p) →ₗ[R] M₂) (h : ∀ x : M, f (Quotient.mk x) = g (Quotient.mk x)) :
-    f = g :=
-  LinearMap.ext fun x => Quotient.inductionOn' x h
-
-/-- The map from a module `M` to the quotient of `M` by a submodule `p` as a linear map. -/
-def mkQ : M →ₗ[R] M ⧸ p where
-  toFun := Quotient.mk
-  map_add' := by simp
-  map_smul' := by simp
-
-@[simp]
-theorem mkQ_apply (x : M) : p.mkQ x = Quotient.mk x :=
-  rfl
-
-theorem mkQ_surjective : Function.Surjective p.mkQ := by
-  rintro ⟨x⟩; exact ⟨x, rfl⟩
-
 theorem strictMono_comap_prod_map :
     StrictMono fun m : Submodule R M ↦ (m.comap p.subtype, m.map p.mkQ) :=
   fun m₁ m₂ ↦ QuotientAddGroup.strictMono_comap_prod_map
@@ -296,14 +121,6 @@ end
 
 variable {R₂ M₂ : Type*} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂}
 
-/-- Two `LinearMap`s from a quotient module are equal if their compositions with
-`submodule.mkQ` are equal.
-
-See note [partially-applied ext lemmas]. -/
-@[ext 1100] -- Porting note: increase priority so this applies before `LinearMap.ext`
-theorem linearMap_qext ⦃f g : M ⧸ p →ₛₗ[τ₁₂] M₂⦄ (h : f.comp p.mkQ = g.comp p.mkQ) : f = g :=
-  LinearMap.ext fun x => Quotient.inductionOn' x <| (LinearMap.congr_fun h : _)
-
 /-- The map from the quotient of `M` by a submodule `p` to `M₂` induced by a linear map `f : M → M₂`
 vanishing on `p`, as a linear map. -/
 def liftQ (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ ker f) : M ⧸ p →ₛₗ[τ₁₂] M₂ :=
@@ -559,24 +376,6 @@ theorem coe_quotEquivOfEqBot_symm (hp : p = ⊥) :
     ((p.quotEquivOfEqBot hp).symm : M →ₗ[R] M ⧸ p) = p.mkQ :=
   rfl
 
-/-- Quotienting by equal submodules gives linearly equivalent quotients. -/
-def quotEquivOfEq (h : p = p') : (M ⧸ p) ≃ₗ[R] M ⧸ p' :=
-  { @Quotient.congr _ _ (quotientRel p) (quotientRel p') (Equiv.refl _) fun a b => by
-      subst h
-      rfl with
-    map_add' := by
-      rintro ⟨x⟩ ⟨y⟩
-      rfl
-    map_smul' := by
-      rintro x ⟨y⟩
-      rfl }
-
-@[simp]
-theorem quotEquivOfEq_mk (h : p = p') (x : M) :
-    Submodule.quotEquivOfEq p p' h (Submodule.Quotient.mk x) =
-      (Submodule.Quotient.mk x) :=
-  rfl
-
 @[simp]
 theorem Quotient.equiv_refl (P : Submodule R M) (Q : Submodule R M)
     (hf : P.map (LinearEquiv.refl R M : M →ₗ[R] M) = Q) :
diff --git a/Mathlib/LinearAlgebra/Quotient/Defs.lean b/Mathlib/LinearAlgebra/Quotient/Defs.lean
new file mode 100644
index 0000000000000..ab4b3b8558678
--- /dev/null
+++ b/Mathlib/LinearAlgebra/Quotient/Defs.lean
@@ -0,0 +1,262 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
+-/
+import Mathlib.Algebra.Module.Submodule.Basic
+import Mathlib.Algebra.Module.Equiv.Defs
+import Mathlib.GroupTheory.QuotientGroup.Defs
+
+/-!
+# Quotients by submodules
+
+* If `p` is a submodule of `M`, `M ⧸ p` is the quotient of `M` with respect to `p`:
+  that is, elements of `M` are identified if their difference is in `p`. This is itself a module.
+
+## Main definitions
+
+ * `Submodule.Quotient.mk`: a function sending an element of `M` to `M ⧸ p`
+ * `Submodule.Quotient.module`: `M ⧸ p` is a module
+ * `Submodule.Quotient.mkQ`: a linear map sending an element of `M` to `M ⧸ p`
+ * `Submodule.quotEquivOfEq`: if `p` and `p'` are equal, their quotients are equivalent
+
+-/
+
+-- For most of this file we work over a noncommutative ring
+section Ring
+
+namespace Submodule
+
+variable {R M : Type*} {r : R} {x y : M} [Ring R] [AddCommGroup M] [Module R M]
+variable (p p' : Submodule R M)
+
+open QuotientAddGroup
+
+/-- The equivalence relation associated to a submodule `p`, defined by `x ≈ y` iff `-x + y ∈ p`.
+
+Note this is equivalent to `y - x ∈ p`, but defined this way to be defeq to the `AddSubgroup`
+version, where commutativity can't be assumed. -/
+def quotientRel : Setoid M :=
+  QuotientAddGroup.leftRel p.toAddSubgroup
+
+theorem quotientRel_def {x y : M} : p.quotientRel x y ↔ x - y ∈ p :=
+  Iff.trans
+    (by
+      rw [leftRel_apply, sub_eq_add_neg, neg_add, neg_neg]
+      rfl)
+    neg_mem_iff
+
+@[deprecated (since := "2024-08-29")] alias quotientRel_r_def := quotientRel_def
+
+/-- The quotient of a module `M` by a submodule `p ⊆ M`. -/
+instance hasQuotient : HasQuotient M (Submodule R M) :=
+  ⟨fun p => Quotient (quotientRel p)⟩
+
+namespace Quotient
+/-- Map associating to an element of `M` the corresponding element of `M/p`,
+when `p` is a submodule of `M`. -/
+def mk {p : Submodule R M} : M → M ⧸ p :=
+  Quotient.mk''
+
+theorem mk'_eq_mk' {p : Submodule R M} (x : M) :
+    @Quotient.mk' _ (quotientRel p) x = mk x :=
+  rfl
+
+theorem mk''_eq_mk {p : Submodule R M} (x : M) : (Quotient.mk'' x : M ⧸ p) = mk x :=
+  rfl
+
+theorem quot_mk_eq_mk {p : Submodule R M} (x : M) : (Quot.mk _ x : M ⧸ p) = mk x :=
+  rfl
+
+protected theorem eq' {x y : M} : (mk x : M ⧸ p) = mk y ↔ -x + y ∈ p :=
+  QuotientAddGroup.eq
+
+protected theorem eq {x y : M} : (mk x : M ⧸ p) = mk y ↔ x - y ∈ p :=
+  (Submodule.Quotient.eq' p).trans (leftRel_apply.symm.trans p.quotientRel_def)
+
+instance : Zero (M ⧸ p) where
+  -- Use Quotient.mk'' instead of mk here because mk is not reducible.
+  -- This would lead to non-defeq diamonds.
+  -- See also the same comment at the One instance for Con.
+  zero := Quotient.mk'' 0
+
+instance : Inhabited (M ⧸ p) :=
+  ⟨0⟩
+
+@[simp]
+theorem mk_zero : mk 0 = (0 : M ⧸ p) :=
+  rfl
+
+@[simp]
+theorem mk_eq_zero : (mk x : M ⧸ p) = 0 ↔ x ∈ p := by simpa using (Quotient.eq' p : mk x = 0 ↔ _)
+
+instance addCommGroup : AddCommGroup (M ⧸ p) :=
+  QuotientAddGroup.Quotient.addCommGroup p.toAddSubgroup
+
+@[simp]
+theorem mk_add : (mk (x + y) : M ⧸ p) = mk x + mk y :=
+  rfl
+
+@[simp]
+theorem mk_neg : (mk (-x) : M ⧸ p) = -(mk x) :=
+  rfl
+
+@[simp]
+theorem mk_sub : (mk (x - y) : M ⧸ p) = mk x - mk y :=
+  rfl
+
+protected nonrec lemma «forall» {P : M ⧸ p → Prop} : (∀ a, P a) ↔ ∀ a, P (mk a) := Quotient.forall
+
+section SMul
+
+variable {S : Type*} [SMul S R] [SMul S M] [IsScalarTower S R M] (P : Submodule R M)
+
+instance instSMul' : SMul S (M ⧸ P) :=
+  ⟨fun a =>
+    Quotient.map' (a • ·) fun x y h =>
+      leftRel_apply.mpr <| by simpa using Submodule.smul_mem P (a • (1 : R)) (leftRel_apply.mp h)⟩
+
+-- Porting note: should this be marked as a `@[default_instance]`?
+/-- Shortcut to help the elaborator in the common case. -/
+instance instSMul : SMul R (M ⧸ P) :=
+  Quotient.instSMul' P
+
+@[simp]
+theorem mk_smul (r : S) (x : M) : (mk (r • x) : M ⧸ p) = r • mk x :=
+  rfl
+
+instance smulCommClass (T : Type*) [SMul T R] [SMul T M] [IsScalarTower T R M]
+    [SMulCommClass S T M] : SMulCommClass S T (M ⧸ P) where
+  smul_comm _x _y := Quotient.ind' fun _z => congr_arg mk (smul_comm _ _ _)
+
+instance isScalarTower (T : Type*) [SMul T R] [SMul T M] [IsScalarTower T R M] [SMul S T]
+    [IsScalarTower S T M] : IsScalarTower S T (M ⧸ P) where
+  smul_assoc _x _y := Quotient.ind' fun _z => congr_arg mk (smul_assoc _ _ _)
+
+instance isCentralScalar [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M]
+    [IsCentralScalar S M] : IsCentralScalar S (M ⧸ P) where
+  op_smul_eq_smul _x := Quotient.ind' fun _z => congr_arg mk <| op_smul_eq_smul _ _
+
+end SMul
+
+section Module
+
+variable {S : Type*}
+
+-- Performance of `Function.Surjective.mulAction` is worse since it has to unify data to apply
+-- TODO: leanprover-community/mathlib4#7432
+instance mulAction' [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M]
+    (P : Submodule R M) : MulAction S (M ⧸ P) :=
+  { Function.Surjective.mulAction mk (surjective_quot_mk _) <| Submodule.Quotient.mk_smul P with
+    toSMul := instSMul' _ }
+
+-- Porting note: should this be marked as a `@[default_instance]`?
+instance mulAction (P : Submodule R M) : MulAction R (M ⧸ P) :=
+  Quotient.mulAction' P
+
+instance smulZeroClass' [SMul S R] [SMulZeroClass S M] [IsScalarTower S R M] (P : Submodule R M) :
+    SMulZeroClass S (M ⧸ P) :=
+  ZeroHom.smulZeroClass ⟨mk, mk_zero _⟩ <| Submodule.Quotient.mk_smul P
+
+-- Porting note: should this be marked as a `@[default_instance]`?
+instance smulZeroClass (P : Submodule R M) : SMulZeroClass R (M ⧸ P) :=
+  Quotient.smulZeroClass' P
+
+-- Performance of `Function.Surjective.distribSMul` is worse since it has to unify data to apply
+-- TODO: leanprover-community/mathlib4#7432
+instance distribSMul' [SMul S R] [DistribSMul S M] [IsScalarTower S R M] (P : Submodule R M) :
+    DistribSMul S (M ⧸ P) :=
+  { Function.Surjective.distribSMul {toFun := mk, map_zero' := rfl, map_add' := fun _ _ => rfl}
+    (surjective_quot_mk _) (Submodule.Quotient.mk_smul P) with
+    toSMulZeroClass := smulZeroClass' _ }
+
+-- Porting note: should this be marked as a `@[default_instance]`?
+instance distribSMul (P : Submodule R M) : DistribSMul R (M ⧸ P) :=
+  Quotient.distribSMul' P
+
+-- Performance of `Function.Surjective.distribMulAction` is worse since it has to unify data
+-- TODO: leanprover-community/mathlib4#7432
+instance distribMulAction' [Monoid S] [SMul S R] [DistribMulAction S M] [IsScalarTower S R M]
+    (P : Submodule R M) : DistribMulAction S (M ⧸ P) :=
+  { Function.Surjective.distribMulAction {toFun := mk, map_zero' := rfl, map_add' := fun _ _ => rfl}
+    (surjective_quot_mk _) (Submodule.Quotient.mk_smul P) with
+    toMulAction := mulAction' _ }
+
+-- Porting note: should this be marked as a `@[default_instance]`?
+instance distribMulAction (P : Submodule R M) : DistribMulAction R (M ⧸ P) :=
+  Quotient.distribMulAction' P
+
+-- Performance of `Function.Surjective.module` is worse since it has to unify data to apply
+-- TODO: leanprover-community/mathlib4#7432
+instance module' [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) :
+    Module S (M ⧸ P) :=
+  { Function.Surjective.module _ {toFun := mk, map_zero' := by rfl, map_add' := fun _ _ => by rfl}
+    (surjective_quot_mk _) (Submodule.Quotient.mk_smul P) with
+    toDistribMulAction := distribMulAction' _ }
+
+-- Porting note: should this be marked as a `@[default_instance]`?
+instance module (P : Submodule R M) : Module R (M ⧸ P) :=
+  Quotient.module' P
+
+end Module
+
+theorem mk_surjective : Function.Surjective (@mk _ _ _ _ _ p) := by
+  rintro ⟨x⟩
+  exact ⟨x, rfl⟩
+
+end Quotient
+
+section
+
+variable {M₂ : Type*} [AddCommGroup M₂] [Module R M₂]
+
+theorem quot_hom_ext (f g : (M ⧸ p) →ₗ[R] M₂) (h : ∀ x : M, f (Quotient.mk x) = g (Quotient.mk x)) :
+    f = g :=
+  LinearMap.ext fun x => Quotient.inductionOn' x h
+
+/-- The map from a module `M` to the quotient of `M` by a submodule `p` as a linear map. -/
+def mkQ : M →ₗ[R] M ⧸ p where
+  toFun := Quotient.mk
+  map_add' := by simp
+  map_smul' := by simp
+
+@[simp]
+theorem mkQ_apply (x : M) : p.mkQ x = Quotient.mk x :=
+  rfl
+
+theorem mkQ_surjective : Function.Surjective p.mkQ := by
+  rintro ⟨x⟩; exact ⟨x, rfl⟩
+
+end
+
+variable {R₂ M₂ : Type*} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂}
+
+/-- Two `LinearMap`s from a quotient module are equal if their compositions with
+`submodule.mkQ` are equal.
+
+See note [partially-applied ext lemmas]. -/
+@[ext 1100] -- Porting note: increase priority so this applies before `LinearMap.ext`
+theorem linearMap_qext ⦃f g : M ⧸ p →ₛₗ[τ₁₂] M₂⦄ (h : f.comp p.mkQ = g.comp p.mkQ) : f = g :=
+  LinearMap.ext fun x => Quotient.inductionOn' x <| (LinearMap.congr_fun h : _)
+
+/-- Quotienting by equal submodules gives linearly equivalent quotients. -/
+def quotEquivOfEq (h : p = p') : (M ⧸ p) ≃ₗ[R] M ⧸ p' :=
+  { @Quotient.congr _ _ (quotientRel p) (quotientRel p') (Equiv.refl _) fun a b => by
+      subst h
+      rfl with
+    map_add' := by
+      rintro ⟨x⟩ ⟨y⟩
+      rfl
+    map_smul' := by
+      rintro x ⟨y⟩
+      rfl }
+
+@[simp]
+theorem quotEquivOfEq_mk (h : p = p') (x : M) :
+    Submodule.quotEquivOfEq p p' h (Submodule.Quotient.mk x) =
+      (Submodule.Quotient.mk x) :=
+  rfl
+
+end Submodule
+
+end Ring
diff --git a/Mathlib/LinearAlgebra/QuotientPi.lean b/Mathlib/LinearAlgebra/Quotient/Pi.lean
similarity index 99%
rename from Mathlib/LinearAlgebra/QuotientPi.lean
rename to Mathlib/LinearAlgebra/Quotient/Pi.lean
index 103b03974aa55..67ac5c5aa2063 100644
--- a/Mathlib/LinearAlgebra/QuotientPi.lean
+++ b/Mathlib/LinearAlgebra/Quotient/Pi.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen, Alex J. Best
 -/
 import Mathlib.LinearAlgebra.Pi
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 
 /-!
 # Submodule quotients and direct sums
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
index f3cea863abf53..ea17f8278672f 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
@@ -6,7 +6,7 @@ Authors: Antoine Chambert-Loir, Jujian Zhang
 
 import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.LinearAlgebra.TensorProduct.Basic
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.LinearAlgebra.Prod
 import Mathlib.RingTheory.Ideal.Quotient
 
diff --git a/Mathlib/MeasureTheory/Constructions/SubmoduleQuotient.lean b/Mathlib/MeasureTheory/Constructions/SubmoduleQuotient.lean
index e5bcc2ccd92dd..711760a5fb963 100644
--- a/Mathlib/MeasureTheory/Constructions/SubmoduleQuotient.lean
+++ b/Mathlib/MeasureTheory/Constructions/SubmoduleQuotient.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Defs
 import Mathlib.MeasureTheory.MeasurableSpace.Basic
 
 /-!
diff --git a/Mathlib/RingTheory/Finiteness.lean b/Mathlib/RingTheory/Finiteness.lean
index fad4868eda18b..74a7408d863d7 100644
--- a/Mathlib/RingTheory/Finiteness.lean
+++ b/Mathlib/RingTheory/Finiteness.lean
@@ -5,12 +5,12 @@ Authors: Johan Commelin
 -/
 import Mathlib.Algebra.Algebra.RestrictScalars
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
-import Mathlib.LinearAlgebra.Quotient
-import Mathlib.LinearAlgebra.StdBasis
 import Mathlib.GroupTheory.Finiteness
+import Mathlib.LinearAlgebra.Basis.Cardinality
+import Mathlib.LinearAlgebra.Quotient.Defs
+import Mathlib.LinearAlgebra.StdBasis
 import Mathlib.RingTheory.Ideal.Maps
 import Mathlib.RingTheory.Nilpotent.Defs
-import Mathlib.LinearAlgebra.Basis.Cardinality
 import Mathlib.Tactic.Algebraize
 
 /-!
diff --git a/Mathlib/RingTheory/Ideal/Colon.lean b/Mathlib/RingTheory/Ideal/Colon.lean
index 9d4dd89b510fc..aaffa3c7acc57 100644
--- a/Mathlib/RingTheory/Ideal/Colon.lean
+++ b/Mathlib/RingTheory/Ideal/Colon.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
 -/
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Defs
 import Mathlib.RingTheory.Ideal.Maps
 
 /-!
diff --git a/Mathlib/RingTheory/Ideal/Quotient.lean b/Mathlib/RingTheory/Ideal/Quotient.lean
index 182a09a1dac95..2cb7713aa5a7d 100644
--- a/Mathlib/RingTheory/Ideal/Quotient.lean
+++ b/Mathlib/RingTheory/Ideal/Quotient.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Chris Hughes, Mario Carneiro, Anne Baanen
 -/
 import Mathlib.GroupTheory.QuotientGroup.Finite
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Defs
 import Mathlib.RingTheory.Congruence.Basic
 import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.Tactic.FinCases
diff --git a/Mathlib/RingTheory/Ideal/QuotientOperations.lean b/Mathlib/RingTheory/Ideal/QuotientOperations.lean
index 972e4cac4a0c1..dba200a53f442 100644
--- a/Mathlib/RingTheory/Ideal/QuotientOperations.lean
+++ b/Mathlib/RingTheory/Ideal/QuotientOperations.lean
@@ -5,6 +5,7 @@ Authors: Kenny Lau, Patrick Massot
 -/
 import Mathlib.Algebra.Algebra.Subalgebra.Operations
 import Mathlib.Algebra.Ring.Fin
+import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.RingTheory.Ideal.Quotient
 
 /-!
diff --git a/Mathlib/RingTheory/IsPrimary.lean b/Mathlib/RingTheory/IsPrimary.lean
index 94ab68398b81e..f4444541b209d 100644
--- a/Mathlib/RingTheory/IsPrimary.lean
+++ b/Mathlib/RingTheory/IsPrimary.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Yakov Pechersky. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 -/
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.RingTheory.Ideal.Operations
 
 /-!
diff --git a/Mathlib/RingTheory/Nilpotent/Lemmas.lean b/Mathlib/RingTheory/Nilpotent/Lemmas.lean
index fdbae3b577172..cfafb9cea8b59 100644
--- a/Mathlib/RingTheory/Nilpotent/Lemmas.lean
+++ b/Mathlib/RingTheory/Nilpotent/Lemmas.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import Mathlib.LinearAlgebra.Matrix.ToLin
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.RingTheory.Ideal.Maps
 import Mathlib.RingTheory.Nilpotent.Defs