Commit 2021-03-11 00:47 c5c97f27

chore(ring_theory/polynomial/basic): remove a use of comap (#6612) This merges together quotient_equiv_quotient_mv_polynomial and quotient_alg_equiv_quotient_mv_polynomial, since the two now have the same domain and codomain. comap was previously needed here to provide a wrapper type with an R-algebra structure on mv_polynomial σ (I.quotient). The updated mv_polynomial.algebra in #6533 transfers the algebra R I.quotient structure directly to mv_polynomial σ I.quotient, eliminating the need for this wrapper type.