refactor(ring_theory/ideal/operations): split quotients to a new file (…

…#18531) This file is growing quite long. Splitting it will reduce dependencies in (some) downstream files, and by becoming shorter also makes this file easier to edit and port. This doesn't attempt to change any proofs in downstream files; instead, it just adds new imports to keep them compiling. There are 9 downstream files which no longer depend on the `quotient_operations` file, although one of these now depends on `ring_theory.ideal.quotient`. A future PR will remove the `ring_theory.ideal.quotient_operations` import from more files. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
leanprover-community · Mar 2, 2023 · e7f0ddb · e7f0ddb
1 parent 9a59dcb
commit e7f0ddb
Show file tree

Hide file tree

Showing 8 changed files with 520 additions and 502 deletions.
diff --git a/src/algebra/direct_limit.lean b/src/algebra/direct_limit.lean
@@ -6,7 +6,7 @@ Authors: Kenny Lau, Chris Hughes
 import data.finset.order
 import algebra.direct_sum.module
 import ring_theory.free_comm_ring
-import ring_theory.ideal.operations
+import ring_theory.ideal.quotient_operations
 /-!
 # Direct limit of modules, abelian groups, rings, and fields.
 

diff --git a/src/analysis/normed/group/quotient.lean b/src/analysis/normed/group/quotient.lean
@@ -5,6 +5,7 @@ Authors: Patrick Massot, Riccardo Brasca
 -/
 import analysis.normed_space.basic
 import analysis.normed.group.hom
+import ring_theory.ideal.quotient_operations
 
 /-!
 # Quotients of seminormed groups

diff --git a/src/ring_theory/finiteness.lean b/src/ring_theory/finiteness.lean
@@ -8,6 +8,7 @@ import algebra.algebra.restrict_scalars
 import algebra.algebra.subalgebra.basic
 import group_theory.finiteness
 import ring_theory.ideal.operations
+import ring_theory.ideal.quotient
 
 /-!
 # Finiteness conditions in commutative algebra

diff --git a/src/ring_theory/ideal/operations.lean b/src/ring_theory/ideal/operations.lean
diff --git a/src/ring_theory/ideal/quotient_operations.lean b/src/ring_theory/ideal/quotient_operations.lean
diff --git a/src/ring_theory/localization/ideal.lean b/src/ring_theory/localization/ideal.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, Mario Carneiro, Johan Commelin, Amelia Livingston, Anne Baanen
 -/
-import ring_theory.ideal.operations
+import ring_theory.ideal.quotient_operations
 import ring_theory.localization.basic
 
 /-!

diff --git a/src/ring_theory/nilpotent.lean b/src/ring_theory/nilpotent.lean
@@ -5,7 +5,7 @@ Authors: Oliver Nash
 -/
 import data.nat.choose.sum
 import algebra.algebra.bilinear
-import ring_theory.ideal.operations
+import ring_theory.ideal.quotient_operations
 
 /-!
 # Nilpotent elements

diff --git a/src/ring_theory/valuation/basic.lean b/src/ring_theory/valuation/basic.lean
@@ -5,7 +5,7 @@ Authors: Kevin Buzzard, Johan Commelin, Patrick Massot
 -/
 
 import algebra.order.with_zero
-import ring_theory.ideal.operations
+import ring_theory.ideal.quotient_operations
 
 /-!