mathlib3

db00ee42 - feat(ring_theory/polynomial/basic): add quotient_equiv_quotient_mv_polynomial (#6287)

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.