# Commit 2022-03-23 12:35 64472d74

View on Github →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.