∀ {σ : Type u_1} {R : Type u_3} [inst : Finite σ] [inst_1 : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R)
  {m : σ →₀ ℕ} {i : σ}, ¬p ∣ m i → (MvPowerSeries.coeff m) ((MvPowerSeries.expand p hp) φ) = 0