∀ (σ : Type u_1) (R : Type u_2) [inst : CommRing R] [inst_1 : Fintype σ] (k : ℕ),
  ∀ a ∈ Finset.antidiagonal k,
    ∑ A ∈ Finset.powersetCard a.1 Finset.univ, ∑ j, MvPolynomial.NewtonIdentities.weight✝ σ R k (A, j) =
      (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2