∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) (p : ℕ) (d : σ →₀ ℕ) (f : MvPowerSeries σ R),
  (MvPowerSeries.coeff d) ((MvPowerSeries.weightedHomogeneousComponent w p) f) =
    if (Finsupp.weight w) d = p then (MvPowerSeries.coeff d) f else 0