Commit 2022-03-23 12:35 64472d74

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) This PR defines the isomorphism between the ring R[a]/I[a] and the ring (R/I[X])/(f mod I) for a a root of the polynomial f with coefficients in R and I an ideal of R. This is useful for proving the Dedekind-Kummer Theorem.