∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  {φ ψ : MvPolynomial σ R} {m n : M} {w : σ → M},
  MvPolynomial.IsWeightedHomogeneous w φ m →
    MvPolynomial.IsWeightedHomogeneous w ψ n → MvPolynomial.IsWeightedHomogeneous w (φ * ψ) (m + n)