Theorem ideal.quotient_equiv_mk

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

feat(ring_theory/polynomial/basic): the isomorphism between `R[a]/I[a]` and `(R/I[X])/(f mod I)` for `a` a root of polynomial `f` and `I` and ideal of `R` (#12646) …