chore(RingTheory/Ideal): split Quotient.lean into Defs and Basic (

#18393) This PR renames and splits files involved in the ideal quotient. Changes: * `RingTheory/Ideal/Quotient.lean` is split into - `RingTheory/Ideal/Quotient/Defs.lean` (definition of ideal quotient and ring structure) * `RingTheory/Ideal/Quotient/Basic.lean` (further results) * `RingTheory/QuotientNilpotent.lean` is renamed to `RingTheory/Ideal/Quotient/Nilpotent.lean` * `RingTheory/QuotientNoetherian.lean` is renamed to `Mathlib/RingTheory/Ideal/Quotient/Noetherian.lean` * `RingTheory/Ideal/QuotientOperations.lean` is renamed to `Mathlib/RingTheory/Ideal/Quotient/Operations.lean` Co-authored-by: Kim Morrison <[email protected]>
leanprover-community · Oct 30, 2024 · abfa430 · abfa430
1 parent 3977332
commit abfa430
Show file tree

Hide file tree

Showing 39 changed files with 237 additions and 185 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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