Vieta's formulas for a family of roots indexed by a finite type

Mathlib reads the coefficients of a product of linear factors off the elementary symmetric functions of the multiset of its roots (Multiset.prod_X_sub_C_coeff). Here the roots are a family x : σ → S indexed by a finite type and the elementary symmetric functions are the values of MvPolynomial.esymm: the k-th elementary symmetric polynomial at x is (-1) ^ k times the coefficient of ∏ i, (X - C (x i)) in degree card σ - k.

Over a domain a monic polynomial of degree card σ whose roots, listed with multiplicity, are the values of x is exactly that product, so the same formula computes its coefficients.

Main results

• MvPolynomial.aeval_esymm_eq_coeff_prod_X_sub_C: the elementary symmetric polynomials at x are the signed coefficients of ∏ i, (X - C (x i)).
• Polynomial.eq_prod_X_sub_C_of_monic_of_roots_eq: a monic polynomial whose roots are listed by x is the product of the linear factors X - C (x i).

theorem MvPolynomial.aeval_esymm_eq_coeff_prod_X_sub_C {σ : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype σ] [CommSemiring R] [CommRing S] [Algebra R S] (x : σ → S) {k : ℕ} (hk : k ≤ Fintype.card σ) : (aeval x) (esymm σ R k) = (-1) ^ k * (∏ i : σ, (Polynomial.X - Polynomial.C (x i))).coeff (Fintype.card σ - k)

Vieta's formulas for an indexed family of roots: the k-th elementary symmetric polynomial, evaluated at x : σ → S, is (-1) ^ k times the coefficient of the monic polynomial ∏ i, (X - C (x i)) in degree card σ - k.

theorem Polynomial.eq_prod_X_sub_C_of_monic_of_roots_eq {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommRing R] [IsDomain R] {f : Polynomial R} {x : σ → R} (hf : f.Monic) (hdeg : f.natDegree = Fintype.card σ) (hroots : f.roots = Multiset.map x Finset.univ.val) : f = ∏ i : σ, (X - C (x i))

A monic polynomial of degree card σ whose roots, with multiplicity, are listed by x : σ → R is the product of the linear factors X - C (x i).