mathlib3

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)

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.