mathlib3

917ab03a - feat(ring_theory/{ideal/basic, adjoin_root): some lemmas from #15000 (#16450)

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. Co-authored-by: Anne Baanen <vierkantor@vierkantor.com>