mathlib3

f5edf469 - chore(ring_theory/finiteness): remove references to `ideal.quotient` (#18538)

chore(ring_theory/finiteness): remove references to `ideal.quotient` (#18538) This proof is not meaningfully more complex, and it removes a dependency that has to be ported before this file can be ported.