∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M} {m : M}
  (n : M) {p : MvPolynomial σ R},
  MvPolynomial.IsWeightedHomogeneous w p m → n ≠ m → (MvPolynomial.weightedHomogeneousComponent w n) p = 0