Newton's identities for a multiset

Mathlib states Newton's identities, MvPolynomial.mul_esymm_eq_sum, for the elementary symmetric and power-sum polynomials in a finite type of variables. This file evaluates them at the elements of a multiset, which is the form in which they apply to the roots of a polynomial: the elementary symmetric functions Multiset.esymm of a multiset are recovered recursively from its power sums (s.map (· ^ j)).sum, in any commutative ring in which the relevant integers can be inverted.

Main results

• Multiset.mul_esymm_eq_sum: Newton's identities for the elements of a multiset.

theorem Multiset.mul_esymm_eq_sum {R : Type u_1} [CommRing R] (s : Multiset R) (k : ℕ) : ↑k * s.esymm k = (-1) ^ (k + 1) * ∑ a ∈ Finset.antidiagonal k with a.1 < k, (-1) ^ a.1 * s.esymm a.1 * (map (fun (x : R) => x ^ a.2) s).sum

Newton's identities for a multiset: k times the k-th elementary symmetric function of the elements of s is an explicit combination of the lower elementary symmetric functions and the power sums (s.map (· ^ j)).sum. This is MvPolynomial.mul_esymm_eq_sum evaluated at the elements of s.