Commit 2020-08-19 17:44 bd5552a3

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