Def adjoin_root.quot_map_of_equiv

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