diff --git a/Mathlib.lean b/Mathlib.lean
index efe0f22301333..f99c43c96a2ad 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4088,8 +4088,11 @@ import Mathlib.RingTheory.Ideal.Over
 import Mathlib.RingTheory.Ideal.Pointwise
 import Mathlib.RingTheory.Ideal.Prime
 import Mathlib.RingTheory.Ideal.Prod
-import Mathlib.RingTheory.Ideal.Quotient
-import Mathlib.RingTheory.Ideal.QuotientOperations
+import Mathlib.RingTheory.Ideal.Quotient.Basic
+import Mathlib.RingTheory.Ideal.Quotient.Defs
+import Mathlib.RingTheory.Ideal.Quotient.Nilpotent
+import Mathlib.RingTheory.Ideal.Quotient.Noetherian
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Ideal.Span
 import Mathlib.RingTheory.Idempotents
 import Mathlib.RingTheory.Int.Basic
@@ -4224,8 +4227,6 @@ import Mathlib.RingTheory.Prime
 import Mathlib.RingTheory.PrimeSpectrum
 import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.RingTheory.QuotSMulTop
-import Mathlib.RingTheory.QuotientNilpotent
-import Mathlib.RingTheory.QuotientNoetherian
 import Mathlib.RingTheory.Radical
 import Mathlib.RingTheory.ReesAlgebra
 import Mathlib.RingTheory.Regular.IsSMulRegular
diff --git a/Mathlib/Algebra/CharP/MixedCharZero.lean b/Mathlib/Algebra/CharP/MixedCharZero.lean
index 71c1c3e90b751..4f9d5da352239 100644
--- a/Mathlib/Algebra/CharP/MixedCharZero.lean
+++ b/Mathlib/Algebra/CharP/MixedCharZero.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Eugster
 -/
 import Mathlib.Algebra.CharP.LocalRing
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.Quotient.Basic
 import Mathlib.Tactic.FieldSimp
 
 /-!
diff --git a/Mathlib/Algebra/CharP/Quotient.lean b/Mathlib/Algebra/CharP/Quotient.lean
index 5f016371c3d73..599a0c714c1b3 100644
--- a/Mathlib/Algebra/CharP/Quotient.lean
+++ b/Mathlib/Algebra/CharP/Quotient.lean
@@ -5,7 +5,7 @@ Authors: Kenny Lau, Eric Wieser
 -/
 import Mathlib.GroupTheory.OrderOfElement
 import Mathlib.RingTheory.Ideal.Maps
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.Quotient.Defs
 
 /-!
 # Characteristic of quotients rings
diff --git a/Mathlib/Algebra/DirectLimit.lean b/Mathlib/Algebra/DirectLimit.lean
index 7788d99fae809..02e8cd959b5e4 100644
--- a/Mathlib/Algebra/DirectLimit.lean
+++ b/Mathlib/Algebra/DirectLimit.lean
@@ -8,7 +8,7 @@ import Mathlib.Data.Finset.Order
 import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.RingTheory.FreeCommRing
 import Mathlib.RingTheory.Ideal.Maps
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.Quotient.Defs
 import Mathlib.Tactic.SuppressCompilation
 
 /-!
diff --git a/Mathlib/Algebra/RingQuot.lean b/Mathlib/Algebra/RingQuot.lean
index e99c9cf279744..fb0556615bab7 100644
--- a/Mathlib/Algebra/RingQuot.lean
+++ b/Mathlib/Algebra/RingQuot.lean
@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Mathlib.Algebra.Algebra.Hom
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Congruence.Basic
+import Mathlib.RingTheory.Ideal.Quotient.Defs
+import Mathlib.RingTheory.Ideal.Span
 
 /-!
 # Quotients of non-commutative rings
diff --git a/Mathlib/Analysis/Normed/Group/Quotient.lean b/Mathlib/Analysis/Normed/Group/Quotient.lean
index 9acc022a5fcfb..f4f3b11f8e753 100644
--- a/Mathlib/Analysis/Normed/Group/Quotient.lean
+++ b/Mathlib/Analysis/Normed/Group/Quotient.lean
@@ -5,7 +5,7 @@ Authors: Patrick Massot, Riccardo Brasca
 -/
 import Mathlib.Analysis.Normed.Module.Basic
 import Mathlib.Analysis.Normed.Group.Hom
-import Mathlib.RingTheory.Ideal.QuotientOperations
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.Topology.MetricSpace.HausdorffDistance
 
 /-!
diff --git a/Mathlib/Analysis/Normed/Ring/Units.lean b/Mathlib/Analysis/Normed/Ring/Units.lean
index 44332541ab81f..0a9b5ef97d8a5 100644
--- a/Mathlib/Analysis/Normed/Ring/Units.lean
+++ b/Mathlib/Analysis/Normed/Ring/Units.lean
@@ -3,8 +3,9 @@ Copyright (c) 2020 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth
 -/
-import Mathlib.Topology.Algebra.Ring.Ideal
 import Mathlib.Analysis.SpecificLimits.Normed
+import Mathlib.Topology.Algebra.Ring.Ideal
+import Mathlib.RingTheory.Ideal.Basic
 
 /-!
 # The group of units of a complete normed ring
diff --git a/Mathlib/Data/ZMod/Quotient.lean b/Mathlib/Data/ZMod/Quotient.lean
index 3ea9499281fd8..031fa4b2b17ad 100644
--- a/Mathlib/Data/ZMod/Quotient.lean
+++ b/Mathlib/Data/ZMod/Quotient.lean
@@ -6,7 +6,7 @@ Authors: Anne Baanen
 import Mathlib.Algebra.Group.Equiv.TypeTags
 import Mathlib.Data.ZMod.Basic
 import Mathlib.GroupTheory.GroupAction.Quotient
-import Mathlib.RingTheory.Ideal.QuotientOperations
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Int.Basic
 import Mathlib.RingTheory.ZMod
 
diff --git a/Mathlib/LinearAlgebra/InvariantBasisNumber.lean b/Mathlib/LinearAlgebra/InvariantBasisNumber.lean
index 1a9f732fb0a95..21a217aa2d30c 100644
--- a/Mathlib/LinearAlgebra/InvariantBasisNumber.lean
+++ b/Mathlib/LinearAlgebra/InvariantBasisNumber.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Kim Morrison
 -/
+import Mathlib.RingTheory.Ideal.Quotient.Basic
 import Mathlib.RingTheory.OrzechProperty
-import Mathlib.RingTheory.Ideal.Quotient
 import Mathlib.RingTheory.PrincipalIdealDomain
 
 /-!
diff --git a/Mathlib/LinearAlgebra/SModEq.lean b/Mathlib/LinearAlgebra/SModEq.lean
index 2c50a7ef8519f..d2851ed817bf6 100644
--- a/Mathlib/LinearAlgebra/SModEq.lean
+++ b/Mathlib/LinearAlgebra/SModEq.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 import Mathlib.Algebra.Polynomial.Eval
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.Quotient.Defs
 
 /-!
 # modular equivalence for submodule
diff --git a/Mathlib/LinearAlgebra/Semisimple.lean b/Mathlib/LinearAlgebra/Semisimple.lean
index 3ec763f056da0..34d9925e6aa6a 100644
--- a/Mathlib/LinearAlgebra/Semisimple.lean
+++ b/Mathlib/LinearAlgebra/Semisimple.lean
@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import Mathlib.FieldTheory.Perfect
-import Mathlib.LinearAlgebra.Basis.VectorSpace
 import Mathlib.LinearAlgebra.AnnihilatingPolynomial
+import Mathlib.LinearAlgebra.Basis.VectorSpace
 import Mathlib.RingTheory.Artinian
-import Mathlib.RingTheory.QuotientNilpotent
+import Mathlib.RingTheory.Ideal.Quotient.Nilpotent
 import Mathlib.RingTheory.SimpleModule
 
 /-!
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
index ea17f8278672f..4ae2be8cf1b11 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir, Jujian Zhang
 -/
 
-import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.LinearAlgebra.TensorProduct.Basic
 import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.LinearAlgebra.Prod
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.RingTheory.Ideal.Quotient.Defs
 
 /-!
 
diff --git a/Mathlib/NumberTheory/Basic.lean b/Mathlib/NumberTheory/Basic.lean
index 5efc33f2496d9..c90ca141f49a5 100644
--- a/Mathlib/NumberTheory/Basic.lean
+++ b/Mathlib/NumberTheory/Basic.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Kenny Lau
 -/
 import Mathlib.Algebra.GeomSum
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.Quotient.Defs
+import Mathlib.RingTheory.Ideal.Span
 
 /-!
 # Basic results in number theory
diff --git a/Mathlib/NumberTheory/Multiplicity.lean b/Mathlib/NumberTheory/Multiplicity.lean
index cfa4de5aac58e..15f1ffc7f450f 100644
--- a/Mathlib/NumberTheory/Multiplicity.lean
+++ b/Mathlib/NumberTheory/Multiplicity.lean
@@ -6,9 +6,11 @@ Authors: Tian Chen, Mantas Bakšys
 import Mathlib.Algebra.GeomSum
 import Mathlib.Algebra.Order.Ring.Basic
 import Mathlib.Algebra.Ring.Int
+import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.Data.Nat.Prime.Int
 import Mathlib.NumberTheory.Padics.PadicVal.Defs
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.Quotient.Defs
+import Mathlib.RingTheory.Ideal.Span
 
 /-!
 # Multiplicity in Number Theory
diff --git a/Mathlib/RingTheory/AdjoinRoot.lean b/Mathlib/RingTheory/AdjoinRoot.lean
index eed173fefa7a8..c9b8dee4c1568 100644
--- a/Mathlib/RingTheory/AdjoinRoot.lean
+++ b/Mathlib/RingTheory/AdjoinRoot.lean
@@ -9,9 +9,9 @@ import Mathlib.FieldTheory.Minpoly.Basic
 import Mathlib.RingTheory.Adjoin.Basic
 import Mathlib.RingTheory.FinitePresentation
 import Mathlib.RingTheory.FiniteType
+import Mathlib.RingTheory.Ideal.Quotient.Noetherian
 import Mathlib.RingTheory.PowerBasis
 import Mathlib.RingTheory.PrincipalIdealDomain
-import Mathlib.RingTheory.QuotientNoetherian
 import Mathlib.RingTheory.Polynomial.Quotient
 
 /-!
diff --git a/Mathlib/RingTheory/Derivation/ToSquareZero.lean b/Mathlib/RingTheory/Derivation/ToSquareZero.lean
index 398d75d13c3f9..e99816f3014ce 100644
--- a/Mathlib/RingTheory/Derivation/ToSquareZero.lean
+++ b/Mathlib/RingTheory/Derivation/ToSquareZero.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nicolò Cavalleri, Andrew Yang
 -/
 import Mathlib.RingTheory.Derivation.Basic
-import Mathlib.RingTheory.Ideal.QuotientOperations
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 
 /-!
 # Results
diff --git a/Mathlib/RingTheory/EisensteinCriterion.lean b/Mathlib/RingTheory/EisensteinCriterion.lean
index 4db4a640eef89..216ad0c0c0a4d 100644
--- a/Mathlib/RingTheory/EisensteinCriterion.lean
+++ b/Mathlib/RingTheory/EisensteinCriterion.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import Mathlib.Data.Nat.Cast.WithTop
-import Mathlib.RingTheory.Prime
+import Mathlib.RingTheory.Ideal.Quotient.Basic
 import Mathlib.RingTheory.Polynomial.Content
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Prime
 
 /-!
 # Eisenstein's criterion
diff --git a/Mathlib/RingTheory/Etale/Basic.lean b/Mathlib/RingTheory/Etale/Basic.lean
index 155276c4c53a6..ca33968558ff3 100644
--- a/Mathlib/RingTheory/Etale/Basic.lean
+++ b/Mathlib/RingTheory/Etale/Basic.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.QuotientNilpotent
+import Mathlib.RingTheory.Ideal.Quotient.Nilpotent
 import Mathlib.RingTheory.Smooth.Basic
 import Mathlib.RingTheory.Unramified.Basic
 
diff --git a/Mathlib/RingTheory/FinitePresentation.lean b/Mathlib/RingTheory/FinitePresentation.lean
index 7aac5e956cc7e..566a54bf9738d 100644
--- a/Mathlib/RingTheory/FinitePresentation.lean
+++ b/Mathlib/RingTheory/FinitePresentation.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import Mathlib.RingTheory.FiniteType
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.MvPolynomial.Tower
-import Mathlib.RingTheory.Ideal.QuotientOperations
 
 /-!
 # Finiteness conditions in commutative algebra
diff --git a/Mathlib/RingTheory/FiniteType.lean b/Mathlib/RingTheory/FiniteType.lean
index 551f8541e5e2a..2f5d0d3bf7abf 100644
--- a/Mathlib/RingTheory/FiniteType.lean
+++ b/Mathlib/RingTheory/FiniteType.lean
@@ -5,7 +5,7 @@ Authors: Johan Commelin
 -/
 import Mathlib.Algebra.FreeAlgebra
 import Mathlib.RingTheory.Adjoin.Tower
-import Mathlib.RingTheory.Ideal.QuotientOperations
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 
 /-!
 # Finiteness conditions in commutative algebra
diff --git a/Mathlib/RingTheory/Flat/FaithfullyFlat.lean b/Mathlib/RingTheory/Flat/FaithfullyFlat.lean
index 0d67c12bacf28..8cd4172217363 100644
--- a/Mathlib/RingTheory/Flat/FaithfullyFlat.lean
+++ b/Mathlib/RingTheory/Flat/FaithfullyFlat.lean
@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Judith Ludwig, Florent Schaffhauser, Yunzhou Xie, Jujian Zhang
 -/
 
-import Mathlib.RingTheory.Flat.Stability
 import Mathlib.LinearAlgebra.TensorProduct.Quotient
+import Mathlib.RingTheory.Flat.Stability
+import Mathlib.RingTheory.Ideal.Quotient.Basic
 
 /-!
 # Faithfully flat modules
diff --git a/Mathlib/RingTheory/Ideal/AssociatedPrime.lean b/Mathlib/RingTheory/Ideal/AssociatedPrime.lean
index 9244156f8bac0..d71a198dceeba 100644
--- a/Mathlib/RingTheory/Ideal/AssociatedPrime.lean
+++ b/Mathlib/RingTheory/Ideal/AssociatedPrime.lean
@@ -5,7 +5,7 @@ Authors: Andrew Yang
 -/
 import Mathlib.LinearAlgebra.Span
 import Mathlib.RingTheory.Ideal.IsPrimary
-import Mathlib.RingTheory.Ideal.QuotientOperations
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Noetherian
 
 /-!
diff --git a/Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean b/Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean
index 2255eaacad2a1..90482f9f393cd 100644
--- a/Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean
+++ b/Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean
@@ -5,7 +5,7 @@ Authors: Yakov Pechersky
 -/
 import Mathlib.LinearAlgebra.Isomorphisms
 import Mathlib.RingTheory.Ideal.Operations
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.Quotient.Defs
 
 /-!
 # Quotients of powers of principal ideals
diff --git a/Mathlib/RingTheory/Ideal/Quotient.lean b/Mathlib/RingTheory/Ideal/Quotient/Basic.lean
similarity index 61%
rename from Mathlib/RingTheory/Ideal/Quotient.lean
rename to Mathlib/RingTheory/Ideal/Quotient/Basic.lean
index 2cb7713aa5a7d..190587bcc84f3 100644
--- a/Mathlib/RingTheory/Ideal/Quotient.lean
+++ b/Mathlib/RingTheory/Ideal/Quotient/Basic.lean
@@ -7,6 +7,7 @@ import Mathlib.GroupTheory.QuotientGroup.Finite
 import Mathlib.LinearAlgebra.Quotient.Defs
 import Mathlib.RingTheory.Congruence.Basic
 import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.RingTheory.Ideal.Quotient.Defs
 import Mathlib.Tactic.FinCases
 
 /-!
@@ -33,41 +34,10 @@ open Set
 variable {R : Type u} [CommRing R] (I : Ideal R) {a b : R}
 variable {S : Type v}
 
--- Note that at present `Ideal` means a left-ideal,
--- so this quotient is only useful in a commutative ring.
--- We should develop quotients by two-sided ideals as well.
-/-- The quotient `R/I` of a ring `R` by an ideal `I`.
-
-The ideal quotient of `I` is defined to equal the quotient of `I` as an `R`-submodule of `R`.
-This definition uses `abbrev` so that typeclass instances can be shared between
-`Ideal.Quotient I` and `Submodule.Quotient I`.
--/
-@[instance] abbrev instHasQuotient : HasQuotient R (Ideal R) :=
-  Submodule.hasQuotient
-
 namespace Quotient
 
 variable {I} {x y : R}
 
-instance one (I : Ideal R) : One (R ⧸ I) :=
-  ⟨Submodule.Quotient.mk 1⟩
-
-/-- On `Ideal`s, `Submodule.quotientRel` is a ring congruence. -/
-protected def ringCon (I : Ideal R) : RingCon R :=
-  { QuotientAddGroup.con I.toAddSubgroup with
-    mul' := fun {a₁ b₁ a₂ b₂} h₁ h₂ => by
-      rw [Submodule.quotientRel_def] at h₁ h₂ ⊢
-      have F := I.add_mem (I.mul_mem_left a₂ h₁) (I.mul_mem_right b₁ h₂)
-      have : a₁ * a₂ - b₁ * b₂ = a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁ := by
-        rw [mul_sub, sub_mul, sub_add_sub_cancel, mul_comm, mul_comm b₁]
-      rwa [← this] at F }
-
-instance commRing (I : Ideal R) : CommRing (R ⧸ I) :=
-    inferInstanceAs (CommRing (Quotient.ringCon I).Quotient)
-
--- Sanity test to make sure no diamonds have emerged in `commRing`
-example : (commRing I).toAddCommGroup = Submodule.Quotient.addCommGroup I := rfl
-
 -- this instance is harder to find than the one via `Algebra α (R ⧸ I)`, so use a lower priority
 instance (priority := 100) isScalarTower_right {α} [SMul α R] [IsScalarTower α R R] :
     IsScalarTower α (R ⧸ I) (R ⧸ I) :=
@@ -81,38 +51,6 @@ instance smulCommClass' {α} [SMul α R] [IsScalarTower α R R] [SMulCommClass R
     SMulCommClass (R ⧸ I) α (R ⧸ I) :=
   (Quotient.ringCon I).smulCommClass'
 
-/-- The ring homomorphism from a ring `R` to a quotient ring `R/I`. -/
-def mk (I : Ideal R) : R →+* R ⧸ I where
-  toFun a := Submodule.Quotient.mk a
-  map_zero' := rfl
-  map_one' := rfl
-  map_mul' _ _ := rfl
-  map_add' _ _ := rfl
-
-instance {I : Ideal R} : Coe R (R ⧸ I) :=
-  ⟨Ideal.Quotient.mk I⟩
-
-/-- Two `RingHom`s from the quotient by an ideal are equal if their
-compositions with `Ideal.Quotient.mk'` are equal.
-
-See note [partially-applied ext lemmas]. -/
-@[ext 1100]
-theorem ringHom_ext [NonAssocSemiring S] ⦃f g : R ⧸ I →+* S⦄ (h : f.comp (mk I) = g.comp (mk I)) :
-    f = g :=
-  RingHom.ext fun x => Quotient.inductionOn' x <| (RingHom.congr_fun h : _)
-
-instance inhabited : Inhabited (R ⧸ I) :=
-  ⟨mk I 37⟩
-
-protected theorem eq : mk I x = mk I y ↔ x - y ∈ I :=
-  Submodule.Quotient.eq I
-
-@[simp]
-theorem mk_eq_mk (x : R) : (Submodule.Quotient.mk x : R ⧸ I) = mk I x := rfl
-
-theorem eq_zero_iff_mem {I : Ideal R} : mk I a = 0 ↔ a ∈ I :=
-  Submodule.Quotient.mk_eq_zero _
-
 theorem eq_zero_iff_dvd (x y : R) : Ideal.Quotient.mk (Ideal.span ({x} : Set R)) y = 0 ↔ x ∣ y := by
   rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]
 
@@ -120,9 +58,6 @@ theorem eq_zero_iff_dvd (x y : R) : Ideal.Quotient.mk (Ideal.span ({x} : Set R))
 lemma mk_singleton_self (x : R) : mk (Ideal.span {x}) x = 0 := by
   rw [eq_zero_iff_dvd]
 
-theorem mk_eq_mk_iff_sub_mem (x y : R) : mk I x = mk I y ↔ x - y ∈ I := by
-  rw [← eq_zero_iff_mem, map_sub, sub_eq_zero]
-
 theorem zero_eq_one_iff {I : Ideal R} : (0 : R ⧸ I) = 1 ↔ I = ⊤ :=
   eq_comm.trans <| eq_zero_iff_mem.trans (eq_top_iff_one _).symm
 
@@ -139,22 +74,6 @@ theorem subsingleton_iff {I : Ideal R} : Subsingleton (R ⧸ I) ↔ I = ⊤ := b
 instance : Unique (R ⧸ (⊤ : Ideal R)) :=
   ⟨⟨0⟩, by rintro ⟨x⟩; exact Quotient.eq_zero_iff_mem.mpr Submodule.mem_top⟩
 
-theorem mk_surjective : Function.Surjective (mk I) := fun y =>
-  Quotient.inductionOn' y fun x => Exists.intro x rfl
-
-instance : RingHomSurjective (mk I) :=
-  ⟨mk_surjective⟩
-
-/-- If `I` is an ideal of a commutative ring `R`, if `q : R → R/I` is the quotient map, and if
-`s ⊆ R` is a subset, then `q⁻¹(q(s)) = ⋃ᵢ(i + s)`, the union running over all `i ∈ I`. -/
-theorem quotient_ring_saturate (I : Ideal R) (s : Set R) :
-    mk I ⁻¹' (mk I '' s) = ⋃ x : I, (fun y => x.1 + y) '' s := by
-  ext x
-  simp only [mem_preimage, mem_image, mem_iUnion, Ideal.Quotient.eq]
-  exact
-    ⟨fun ⟨a, a_in, h⟩ => ⟨⟨_, I.neg_mem h⟩, a, a_in, by simp⟩, fun ⟨⟨i, hi⟩, a, ha, Eq⟩ =>
-      ⟨a, ha, by rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]; exact I.neg_mem hi⟩⟩
-
 instance noZeroDivisors (I : Ideal R) [hI : I.IsPrime] : NoZeroDivisors (R ⧸ I) where
     eq_zero_or_eq_zero_of_mul_eq_zero {a b} := Quotient.inductionOn₂' a b fun {_ _} hab =>
       (hI.mem_or_mem (eq_zero_iff_mem.1 hab)).elim (Or.inl ∘ eq_zero_iff_mem.2)
@@ -225,63 +144,8 @@ theorem maximal_ideal_iff_isField_quotient (I : Ideal R) : I.IsMaximal ↔ IsFie
     Field.toIsField _,
     maximal_of_isField _⟩
 
-variable [Semiring S]
-
-/-- Given a ring homomorphism `f : R →+* S` sending all elements of an ideal to zero,
-lift it to the quotient by this ideal. -/
-def lift (I : Ideal R) (f : R →+* S) (H : ∀ a : R, a ∈ I → f a = 0) : R ⧸ I →+* S :=
-  { QuotientAddGroup.lift I.toAddSubgroup f.toAddMonoidHom H with
-    map_one' := f.map_one
-    map_mul' := fun a₁ a₂ => Quotient.inductionOn₂' a₁ a₂ f.map_mul }
-
-@[simp]
-theorem lift_mk (I : Ideal R) (f : R →+* S) (H : ∀ a : R, a ∈ I → f a = 0) :
-    lift I f H (mk I a) = f a :=
-  rfl
-
-theorem lift_surjective_of_surjective (I : Ideal R) {f : R →+* S} (H : ∀ a : R, a ∈ I → f a = 0)
-    (hf : Function.Surjective f) : Function.Surjective (Ideal.Quotient.lift I f H) := by
-  intro y
-  obtain ⟨x, rfl⟩ := hf y
-  use Ideal.Quotient.mk I x
-  simp only [Ideal.Quotient.lift_mk]
-
-/-- The ring homomorphism from the quotient by a smaller ideal to the quotient by a larger ideal.
-
-This is the `Ideal.Quotient` version of `Quot.Factor` -/
-def factor (S T : Ideal R) (H : S ≤ T) : R ⧸ S →+* R ⧸ T :=
-  Ideal.Quotient.lift S (mk T) fun _ hx => eq_zero_iff_mem.2 (H hx)
-
-@[simp]
-theorem factor_mk (S T : Ideal R) (H : S ≤ T) (x : R) : factor S T H (mk S x) = mk T x :=
-  rfl
-
-@[simp]
-theorem factor_comp_mk (S T : Ideal R) (H : S ≤ T) : (factor S T H).comp (mk S) = mk T := by
-  ext x
-  rw [RingHom.comp_apply, factor_mk]
-
 end Quotient
 
-/-- Quotienting by equal ideals gives equivalent rings.
-
-See also `Submodule.quotEquivOfEq` and `Ideal.quotientEquivAlgOfEq`.
--/
-def quotEquivOfEq {R : Type*} [CommRing R] {I J : Ideal R} (h : I = J) : R ⧸ I ≃+* R ⧸ J :=
-  { Submodule.quotEquivOfEq I J h with
-    map_mul' := by
-      rintro ⟨x⟩ ⟨y⟩
-      rfl }
-
-@[simp]
-theorem quotEquivOfEq_mk {R : Type*} [CommRing R] {I J : Ideal R} (h : I = J) (x : R) :
-    quotEquivOfEq h (Ideal.Quotient.mk I x) = Ideal.Quotient.mk J x :=
-  rfl
-
-@[simp]
-theorem quotEquivOfEq_symm {R : Type*} [CommRing R] {I J : Ideal R} (h : I = J) :
-    (Ideal.quotEquivOfEq h).symm = Ideal.quotEquivOfEq h.symm := by ext; rfl
-
 section Pi
 
 variable (ι : Type v)
diff --git a/Mathlib/RingTheory/Ideal/Quotient/Defs.lean b/Mathlib/RingTheory/Ideal/Quotient/Defs.lean
new file mode 100644
index 0000000000000..16ccd620390d8
--- /dev/null
+++ b/Mathlib/RingTheory/Ideal/Quotient/Defs.lean
@@ -0,0 +1,180 @@
+/-
+Copyright (c) 2018 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau, Chris Hughes, Mario Carneiro, Anne Baanen
+-/
+import Mathlib.LinearAlgebra.Quotient.Defs
+import Mathlib.RingTheory.Congruence.Defs
+import Mathlib.RingTheory.Ideal.Defs
+
+/-!
+# Ideal quotients
+
+This file defines ideal quotients as a special case of submodule quotients and proves some basic
+results about these quotients.
+
+See `Algebra.RingQuot` for quotients of non-commutative rings.
+
+## Main definitions
+
+ - `Ideal.instHasQuotient`: the quotient of a commutative ring `R` by an ideal `I : Ideal R`
+ - `Ideal.Quotient.commRing`: the ring structure of the ideal quotient
+ - `Ideal.Quotient.mk`: map an element of `R` to the quotient `R ⧸ I`
+ - `Ideal.Quotient.lift`: turn a map `R → S` into a map `R ⧸ I → S`
+ - `Ideal.quotEquivOfEq`: quotienting by equal ideals gives isomorphic rings
+-/
+
+
+universe u v w
+
+namespace Ideal
+
+open Set
+
+variable {R : Type u} [CommRing R] (I : Ideal R) {a b : R}
+variable {S : Type v}
+
+-- Note that at present `Ideal` means a left-ideal,
+-- so this quotient is only useful in a commutative ring.
+-- We should develop quotients by two-sided ideals as well.
+/-- The quotient `R/I` of a ring `R` by an ideal `I`.
+
+The ideal quotient of `I` is defined to equal the quotient of `I` as an `R`-submodule of `R`.
+This definition uses `abbrev` so that typeclass instances can be shared between
+`Ideal.Quotient I` and `Submodule.Quotient I`.
+-/
+@[instance] abbrev instHasQuotient : HasQuotient R (Ideal R) :=
+  Submodule.hasQuotient
+
+namespace Quotient
+
+variable {I} {x y : R}
+
+instance one (I : Ideal R) : One (R ⧸ I) :=
+  ⟨Submodule.Quotient.mk 1⟩
+
+/-- On `Ideal`s, `Submodule.quotientRel` is a ring congruence. -/
+protected def ringCon (I : Ideal R) : RingCon R :=
+  { QuotientAddGroup.con I.toAddSubgroup with
+    mul' := fun {a₁ b₁ a₂ b₂} h₁ h₂ => by
+      rw [Submodule.quotientRel_def] at h₁ h₂ ⊢
+      have F := I.add_mem (I.mul_mem_left a₂ h₁) (I.mul_mem_right b₁ h₂)
+      have : a₁ * a₂ - b₁ * b₂ = a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁ := by
+        rw [mul_sub, sub_mul, sub_add_sub_cancel, mul_comm, mul_comm b₁]
+      rwa [← this] at F }
+
+instance commRing (I : Ideal R) : CommRing (R ⧸ I) :=
+    inferInstanceAs (CommRing (Quotient.ringCon I).Quotient)
+
+-- Sanity test to make sure no diamonds have emerged in `commRing`
+example : (commRing I).toAddCommGroup = Submodule.Quotient.addCommGroup I := rfl
+
+/-- The ring homomorphism from a ring `R` to a quotient ring `R/I`. -/
+def mk (I : Ideal R) : R →+* R ⧸ I where
+  toFun a := Submodule.Quotient.mk a
+  map_zero' := rfl
+  map_one' := rfl
+  map_mul' _ _ := rfl
+  map_add' _ _ := rfl
+
+instance {I : Ideal R} : Coe R (R ⧸ I) :=
+  ⟨Ideal.Quotient.mk I⟩
+
+/-- Two `RingHom`s from the quotient by an ideal are equal if their
+compositions with `Ideal.Quotient.mk'` are equal.
+
+See note [partially-applied ext lemmas]. -/
+@[ext 1100]
+theorem ringHom_ext [NonAssocSemiring S] ⦃f g : R ⧸ I →+* S⦄ (h : f.comp (mk I) = g.comp (mk I)) :
+    f = g :=
+  RingHom.ext fun x => Quotient.inductionOn' x <| (RingHom.congr_fun h : _)
+
+instance inhabited : Inhabited (R ⧸ I) :=
+  ⟨mk I 37⟩
+
+protected theorem eq : mk I x = mk I y ↔ x - y ∈ I :=
+  Submodule.Quotient.eq I
+
+@[simp]
+theorem mk_eq_mk (x : R) : (Submodule.Quotient.mk x : R ⧸ I) = mk I x := rfl
+
+theorem eq_zero_iff_mem {I : Ideal R} : mk I a = 0 ↔ a ∈ I :=
+  Submodule.Quotient.mk_eq_zero _
+
+theorem mk_eq_mk_iff_sub_mem (x y : R) : mk I x = mk I y ↔ x - y ∈ I := by
+  rw [← eq_zero_iff_mem, map_sub, sub_eq_zero]
+
+theorem mk_surjective : Function.Surjective (mk I) := fun y =>
+  Quotient.inductionOn' y fun x => Exists.intro x rfl
+
+instance : RingHomSurjective (mk I) :=
+  ⟨mk_surjective⟩
+
+/-- If `I` is an ideal of a commutative ring `R`, if `q : R → R/I` is the quotient map, and if
+`s ⊆ R` is a subset, then `q⁻¹(q(s)) = ⋃ᵢ(i + s)`, the union running over all `i ∈ I`. -/
+theorem quotient_ring_saturate (I : Ideal R) (s : Set R) :
+    mk I ⁻¹' (mk I '' s) = ⋃ x : I, (fun y => x.1 + y) '' s := by
+  ext x
+  simp only [mem_preimage, mem_image, mem_iUnion, Ideal.Quotient.eq]
+  exact
+    ⟨fun ⟨a, a_in, h⟩ => ⟨⟨_, I.neg_mem h⟩, a, a_in, by simp⟩, fun ⟨⟨i, hi⟩, a, ha, Eq⟩ =>
+      ⟨a, ha, by rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]; exact I.neg_mem hi⟩⟩
+
+variable [Semiring S]
+
+/-- Given a ring homomorphism `f : R →+* S` sending all elements of an ideal to zero,
+lift it to the quotient by this ideal. -/
+def lift (I : Ideal R) (f : R →+* S) (H : ∀ a : R, a ∈ I → f a = 0) : R ⧸ I →+* S :=
+  { QuotientAddGroup.lift I.toAddSubgroup f.toAddMonoidHom H with
+    map_one' := f.map_one
+    map_mul' := fun a₁ a₂ => Quotient.inductionOn₂' a₁ a₂ f.map_mul }
+
+@[simp]
+theorem lift_mk (I : Ideal R) (f : R →+* S) (H : ∀ a : R, a ∈ I → f a = 0) :
+    lift I f H (mk I a) = f a :=
+  rfl
+
+theorem lift_surjective_of_surjective (I : Ideal R) {f : R →+* S} (H : ∀ a : R, a ∈ I → f a = 0)
+    (hf : Function.Surjective f) : Function.Surjective (Ideal.Quotient.lift I f H) := by
+  intro y
+  obtain ⟨x, rfl⟩ := hf y
+  use Ideal.Quotient.mk I x
+  simp only [Ideal.Quotient.lift_mk]
+
+/-- The ring homomorphism from the quotient by a smaller ideal to the quotient by a larger ideal.
+
+This is the `Ideal.Quotient` version of `Quot.Factor` -/
+def factor (S T : Ideal R) (H : S ≤ T) : R ⧸ S →+* R ⧸ T :=
+  Ideal.Quotient.lift S (mk T) fun _ hx => eq_zero_iff_mem.2 (H hx)
+
+@[simp]
+theorem factor_mk (S T : Ideal R) (H : S ≤ T) (x : R) : factor S T H (mk S x) = mk T x :=
+  rfl
+
+@[simp]
+theorem factor_comp_mk (S T : Ideal R) (H : S ≤ T) : (factor S T H).comp (mk S) = mk T := by
+  ext x
+  rw [RingHom.comp_apply, factor_mk]
+
+end Quotient
+
+/-- Quotienting by equal ideals gives equivalent rings.
+
+See also `Submodule.quotEquivOfEq` and `Ideal.quotientEquivAlgOfEq`.
+-/
+def quotEquivOfEq {R : Type*} [CommRing R] {I J : Ideal R} (h : I = J) : R ⧸ I ≃+* R ⧸ J :=
+  { Submodule.quotEquivOfEq I J h with
+    map_mul' := by
+      rintro ⟨x⟩ ⟨y⟩
+      rfl }
+
+@[simp]
+theorem quotEquivOfEq_mk {R : Type*} [CommRing R] {I J : Ideal R} (h : I = J) (x : R) :
+    quotEquivOfEq h (Ideal.Quotient.mk I x) = Ideal.Quotient.mk J x :=
+  rfl
+
+@[simp]
+theorem quotEquivOfEq_symm {R : Type*} [CommRing R] {I J : Ideal R} (h : I = J) :
+    (Ideal.quotEquivOfEq h).symm = Ideal.quotEquivOfEq h.symm := by ext; rfl
+
+end Ideal
diff --git a/Mathlib/RingTheory/QuotientNilpotent.lean b/Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean
similarity index 98%
rename from Mathlib/RingTheory/QuotientNilpotent.lean
rename to Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean
index 79300ab5bd018..f37051e0c6331 100644
--- a/Mathlib/RingTheory/QuotientNilpotent.lean
+++ b/Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Nilpotent.Lemmas
-import Mathlib.RingTheory.Ideal.QuotientOperations
 
 /-!
 # Nilpotent elements in quotient rings
diff --git a/Mathlib/RingTheory/QuotientNoetherian.lean b/Mathlib/RingTheory/Ideal/Quotient/Noetherian.lean
similarity index 89%
rename from Mathlib/RingTheory/QuotientNoetherian.lean
rename to Mathlib/RingTheory/Ideal/Quotient/Noetherian.lean
index b8a7d3337c213..e60aaec70aca0 100644
--- a/Mathlib/RingTheory/QuotientNoetherian.lean
+++ b/Mathlib/RingTheory/Ideal/Quotient/Noetherian.lean
@@ -3,8 +3,8 @@ Copyright (c) 2021 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Noetherian
-import Mathlib.RingTheory.Ideal.QuotientOperations
 
 /-!
 # Noetherian quotient rings and quotient modules
diff --git a/Mathlib/RingTheory/Ideal/QuotientOperations.lean b/Mathlib/RingTheory/Ideal/Quotient/Operations.lean
similarity index 99%
rename from Mathlib/RingTheory/Ideal/QuotientOperations.lean
rename to Mathlib/RingTheory/Ideal/Quotient/Operations.lean
index dba200a53f442..20fe91eb1a90e 100644
--- a/Mathlib/RingTheory/Ideal/QuotientOperations.lean
+++ b/Mathlib/RingTheory/Ideal/Quotient/Operations.lean
@@ -6,7 +6,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
+import Mathlib.RingTheory.Ideal.Quotient.Basic
 
 /-!
 # More operations on modules and ideals related to quotients
diff --git a/Mathlib/RingTheory/Idempotents.lean b/Mathlib/RingTheory/Idempotents.lean
index 958157f3ad00b..ffc85853ec287 100644
--- a/Mathlib/RingTheory/Idempotents.lean
+++ b/Mathlib/RingTheory/Idempotents.lean
@@ -5,7 +5,7 @@ Authors: Andrew Yang
 -/
 import Mathlib.Algebra.GeomSum
 import Mathlib.Algebra.Polynomial.AlgebraMap
-import Mathlib.RingTheory.Ideal.QuotientOperations
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Nilpotent.Defs
 
 /-!
diff --git a/Mathlib/RingTheory/JacobsonIdeal.lean b/Mathlib/RingTheory/JacobsonIdeal.lean
index 4da503125fb46..0597e9532b91d 100644
--- a/Mathlib/RingTheory/JacobsonIdeal.lean
+++ b/Mathlib/RingTheory/JacobsonIdeal.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Devon Tuma, Wojciech Nawrocki
 -/
 import Mathlib.RingTheory.Ideal.IsPrimary
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.Quotient.Basic
 import Mathlib.RingTheory.Polynomial.Quotient
 import Mathlib.RingTheory.TwoSidedIdeal.Operations
 
diff --git a/Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean b/Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean
index 77da457b5bff8..0d585ff2970c0 100644
--- a/Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean
+++ b/Mathlib/RingTheory/LocalRing/ResidueField/Defs.lean
@@ -3,8 +3,8 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Chris Hughes, Mario Carneiro
 -/
+import Mathlib.RingTheory.Ideal.Quotient.Basic
 import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
-import Mathlib.RingTheory.Ideal.Quotient
 
 /-!
 
diff --git a/Mathlib/RingTheory/Localization/Ideal.lean b/Mathlib/RingTheory/Localization/Ideal.lean
index dfcf60e25dc37..4d5fd06147aed 100644
--- a/Mathlib/RingTheory/Localization/Ideal.lean
+++ b/Mathlib/RingTheory/Localization/Ideal.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Mario Carneiro, Johan Commelin, Amelia Livingston, Anne Baanen
 -/
 import Mathlib.GroupTheory.MonoidLocalization.Away
-import Mathlib.RingTheory.Ideal.QuotientOperations
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Localization.Basic
 
 /-!
diff --git a/Mathlib/RingTheory/MvPolynomial/Localization.lean b/Mathlib/RingTheory/MvPolynomial/Localization.lean
index 0eb65b979682d..2a8977ca29026 100644
--- a/Mathlib/RingTheory/MvPolynomial/Localization.lean
+++ b/Mathlib/RingTheory/MvPolynomial/Localization.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christian Merten
 -/
 import Mathlib.Algebra.MvPolynomial.CommRing
-import Mathlib.RingTheory.Ideal.QuotientOperations
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Localization.Away.Basic
 import Mathlib.RingTheory.Localization.Basic
 import Mathlib.RingTheory.MvPolynomial.Basic
diff --git a/Mathlib/RingTheory/Polynomial/Nilpotent.lean b/Mathlib/RingTheory/Polynomial/Nilpotent.lean
index 1579b65f458f9..a921d48c10bc8 100644
--- a/Mathlib/RingTheory/Polynomial/Nilpotent.lean
+++ b/Mathlib/RingTheory/Polynomial/Nilpotent.lean
@@ -6,10 +6,10 @@ Authors: Emilie Uthaiwat, Oliver Nash
 import Mathlib.Algebra.Polynomial.AlgebraMap
 import Mathlib.Algebra.Polynomial.Div
 import Mathlib.Algebra.Polynomial.Identities
-import Mathlib.RingTheory.Ideal.QuotientOperations
+import Mathlib.RingTheory.Ideal.Quotient.Operations
+import Mathlib.RingTheory.Nilpotent.Basic
 import Mathlib.RingTheory.Nilpotent.Lemmas
 import Mathlib.RingTheory.Polynomial.Tower
-import Mathlib.RingTheory.Nilpotent.Basic
 
 /-!
 # Nilpotency in polynomial rings.
diff --git a/Mathlib/RingTheory/Polynomial/Quotient.lean b/Mathlib/RingTheory/Polynomial/Quotient.lean
index 6e25993471670..7b81b10264dcd 100644
--- a/Mathlib/RingTheory/Polynomial/Quotient.lean
+++ b/Mathlib/RingTheory/Polynomial/Quotient.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, David Kurniadi Angdinata, Devon Tuma, Riccardo Brasca
 -/
 import Mathlib.Algebra.Polynomial.Div
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Polynomial.Basic
-import Mathlib.RingTheory.Ideal.QuotientOperations
 
 /-!
 # Quotients of polynomial rings
diff --git a/Mathlib/RingTheory/Smooth/Basic.lean b/Mathlib/RingTheory/Smooth/Basic.lean
index 30f395c764148..2f26235f7f9cd 100644
--- a/Mathlib/RingTheory/Smooth/Basic.lean
+++ b/Mathlib/RingTheory/Smooth/Basic.lean
@@ -3,13 +3,13 @@ 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.Ideal.Cotangent
-import Mathlib.RingTheory.QuotientNilpotent
-import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.RingTheory.FinitePresentation
 import Mathlib.RingTheory.FiniteStability
-import Mathlib.RingTheory.Localization.Away.Basic
+import Mathlib.RingTheory.Ideal.Cotangent
+import Mathlib.RingTheory.Ideal.Quotient.Nilpotent
 import Mathlib.RingTheory.Localization.Away.AdjoinRoot
+import Mathlib.RingTheory.Localization.Away.Basic
+import Mathlib.RingTheory.TensorProduct.Basic
 
 /-!
 
diff --git a/Mathlib/RingTheory/Unramified/Basic.lean b/Mathlib/RingTheory/Unramified/Basic.lean
index 6b6f3781f7e4b..73ca2ac3c5f04 100644
--- a/Mathlib/RingTheory/Unramified/Basic.lean
+++ b/Mathlib/RingTheory/Unramified/Basic.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.RingTheory.FiniteStability
-import Mathlib.RingTheory.Localization.Away.AdjoinRoot
-import Mathlib.RingTheory.QuotientNilpotent
+import Mathlib.RingTheory.Ideal.Quotient.Nilpotent
 import Mathlib.RingTheory.Kaehler.Basic
+import Mathlib.RingTheory.Localization.Away.AdjoinRoot
 
 /-!
 
diff --git a/Mathlib/RingTheory/Valuation/Quotient.lean b/Mathlib/RingTheory/Valuation/Quotient.lean
index c246dfce6f64c..a39ad50baf226 100644
--- a/Mathlib/RingTheory/Valuation/Quotient.lean
+++ b/Mathlib/RingTheory/Valuation/Quotient.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Johan Commelin, Patrick Massot
 -/
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Valuation.Basic
-import Mathlib.RingTheory.Ideal.QuotientOperations
 
 /-!
 # The valuation on a quotient ring
diff --git a/Mathlib/Topology/Algebra/Ring/Ideal.lean b/Mathlib/Topology/Algebra/Ring/Ideal.lean
index 28afb07beedb3..b6224bda75b37 100644
--- a/Mathlib/Topology/Algebra/Ring/Ideal.lean
+++ b/Mathlib/Topology/Algebra/Ring/Ideal.lean
@@ -5,7 +5,7 @@ Authors: Patrick Massot
 -/
 import Mathlib.Topology.Algebra.Ring.Basic
 import Mathlib.Topology.Algebra.Group.Quotient
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.Quotient.Defs
 
 /-!
 # Ideals and quotients of topological rings