Theorem adjoin_root.polynomial.quot_quot_equiv_comm_mk_mk

feat(ring_theory/adjoin_root): a bit of missing API for maps between certain quotients of `adjoin_root f` (#15757) …

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) …