∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M}
  (φ : MvPolynomial σ R) (n : M) (r : R),
  (MvPolynomial.weightedHomogeneousComponent w n) (MvPolynomial.C r * φ) =
    MvPolynomial.C r * (MvPolynomial.weightedHomogeneousComponent w n) φ