∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (φ : MvPolynomial σ R) (n : ℕ) (r : R),
  (MvPolynomial.homogeneousComponent n) (MvPolynomial.C r * φ) =
    MvPolynomial.C r * (MvPolynomial.homogeneousComponent n) φ