Theorems · Theorem · commutative algebra

MvPolynomial.mul_esymm_eq_sum

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

Newton's identities give a recurrence relation for the kth elementary symmetric polynomial in terms of lower degree elementary symmetric polynomials and power sums.

Defined in

Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeCommRing