Commit 2023-03-02 07:01 e7f0ddbf

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.