Commit 2021-10-22 13:16 b812fb9c

refactor(ring_theory/ideal): split off quotient.lean (#9850) Both ring_theory/ideal/basic.lean and ring_theory/ideal/operations.lean were starting to get a bit long, so I split off the definition of ideal.quotient and the results that had no further dependencies. I also went through all the imports for files depending on either ideal/basic.lean or ideal/operations.lean to check whether they shouldn't depend on ideal/quotient.lean instead.