∀ {S₁ : Type u_2} {S₂ : Type u_3} (σ : Type u_1) [inst : CommSemiring S₁] [inst_1 : CommSemiring S₂] (e : S₁ ≃+* S₂)
  (x y : MvPolynomial σ S₁),
  (↑↑(MvPolynomial.map ↑e)).toFun (x * y) = (↑↑(MvPolynomial.map ↑e)).toFun x * (↑↑(MvPolynomial.map ↑e)).toFun y