mathlib3

bd5552a3 - feat(ring_theory/polynomial/basic): Isomorphism between polynomials over a quotient and quotient over polynomials (#3847)

feat(ring_theory/polynomial/basic): Isomorphism between polynomials over a quotient and quotient over polynomials (#3847) The main statement is `polynomial_quotient_equiv_quotient_polynomial`, which gives that If `I` is an ideal of `R`, then the ring polynomials over the quotient ring `I.quotient` is isomorphic to the quotient of `polynomial R` by the ideal `map C I`. Also, `mem_map_C_iff` shows that `map C I` contains exactly the polynomials whose coefficients all lie in `I`