mathlib

c5c97f27 - chore(ring_theory/polynomial/basic): remove a use of comap (#6612)

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.