Commit 2022-09-15 11:57 2178a7f7

feat(ring_theory/{ideal/basic, adjoin_root): some lemmas from #15000 (#16450) This PR contains some lemmas that were originally in #15000. The main result that is proven here is quotient_equiv_quotient_minpoly_map, which says that if α has minimal polynomial f over R and I is an ideal of R, then rings R[α] / I[α] and (R/I)[X] / (f mod I) are isomorphic as R-algebras.