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.





leanprover-community/mathlib,leanprover-community/mathlib