Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes