Theorems · Theorem · commutative algebra

MvPolynomial.psum_eq_mul_esymm_sub_sum

∀ (σ : Type u_1) [inst : Fintype σ] (R : Type u_2) [inst_1 : CommRing R] (k : ℕ),
  0 < k →
    MvPolynomial.psum σ R k =
      (-1) ^ (k + 1) * ↑k * MvPolynomial.esymm σ R k -
        ∑ a ∈ Finset.HasAntidiagonal.antidiagonal k with a.1 ∈ Set.Ioo 0 k,
          (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2

A version of Newton's identities which may be more useful in the case that we know the values of the elementary symmetric polynomials and would like to calculate the values of the power sums.

Defined in

Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Cited by

0 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeCommRing