∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R],
  MvPolynomial.sumRingEquiv R S₁ S₂ =
    MvPolynomial.mvPolynomialEquivMvPolynomial R (S₁ ⊕ S₂) S₁ (MvPolynomial S₂ R) (MvPolynomial.sumToIter R S₁ S₂)
      (MvPolynomial.iterToSum R S₁ S₂) ⋯ ⋯ ⋯ ⋯