Commit 2021-02-22 18:48 db00ee42

feat(ring_theory/polynomial/basic): add quotient_equiv_quotient_mv_polynomial (#6287) I've added quotient_equiv_quotient_mv_polynomial that says that (R/I)[x_i] ≃+* (R[x_i])/I where I is an ideal of R. I've included also a version for R-algebras. The proof is very similar to the case of (one variable) polynomials.