mathlib

e7f0ddbf - refactor(ring_theory/ideal/operations): split quotients to a new file (#18531)

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>