# Vieta's Formula #

The main result is Multiset.prod_X_add_C_eq_sum_esymm, which shows that the product of linear terms X + λ with λ in a Multiset s is equal to a linear combination of the symmetric functions esymm s.

From this, we deduce MvPolynomial.prod_X_add_C_eq_sum_esymm which is the equivalent formula for the product of linear terms X + X i with i in a Fintype σ as a linear combination of the symmetric polynomials esymm σ R j.

For R be an integral domain (so that p.roots is defined for any p : R[X] as a multiset), we derive Polynomial.coeff_eq_esymm_roots_of_card, the relationship between the coefficients and the roots of p for a polynomial p that splits (i.e. having as many roots as its degree).

theorem Multiset.prod_X_add_C_eq_sum_esymm {R : Type u_1} [] (s : ) :
Multiset.prod (Multiset.map (fun (r : R) => Polynomial.X + Polynomial.C r) s) = Finset.sum (Finset.range (Multiset.card s + 1)) fun (j : ) => Polynomial.C () * Polynomial.X ^ (Multiset.card s - j)

A sum version of Vieta's formula for Multiset: the product of the linear terms X + λ where λ runs through a multiset s is equal to a linear combination of the symmetric functions esymm s of the λ's .

theorem Multiset.prod_X_add_C_coeff {R : Type u_1} [] (s : ) {k : } (h : k Multiset.card s) :
Polynomial.coeff (Multiset.prod (Multiset.map (fun (r : R) => Polynomial.X + Polynomial.C r) s)) k = Multiset.esymm s (Multiset.card s - k)

Vieta's formula for the coefficients of the product of linear terms X + λ where λ runs through a multiset s : the kth coefficient is the symmetric function esymm (card s - k) s.

theorem Multiset.prod_X_add_C_coeff' {R : Type u_1} [] {σ : Type u_2} (s : ) (r : σR) {k : } (h : k Multiset.card s) :
Polynomial.coeff (Multiset.prod (Multiset.map (fun (i : σ) => Polynomial.X + Polynomial.C (r i)) s)) k = Multiset.esymm () (Multiset.card s - k)
theorem Finset.prod_X_add_C_coeff {R : Type u_1} [] {σ : Type u_2} (s : ) (r : σR) {k : } (h : k s.card) :
Polynomial.coeff (Finset.prod s fun (i : σ) => Polynomial.X + Polynomial.C (r i)) k = Finset.sum (Finset.powersetCard (s.card - k) s) fun (t : ) => Finset.prod t fun (i : σ) => r i
theorem Multiset.esymm_neg {R : Type u_1} [] (s : ) (k : ) :
Multiset.esymm (Multiset.map Neg.neg s) k = (-1) ^ k *
theorem Multiset.prod_X_sub_X_eq_sum_esymm {R : Type u_1} [] (s : ) :
Multiset.prod (Multiset.map (fun (t : R) => Polynomial.X - Polynomial.C t) s) = Finset.sum (Finset.range (Multiset.card s + 1)) fun (j : ) => (-1) ^ j * (Polynomial.C () * Polynomial.X ^ (Multiset.card s - j))
theorem Multiset.prod_X_sub_C_coeff {R : Type u_1} [] (s : ) {k : } (h : k Multiset.card s) :
Polynomial.coeff (Multiset.prod (Multiset.map (fun (t : R) => Polynomial.X - Polynomial.C t) s)) k = (-1) ^ (Multiset.card s - k) * Multiset.esymm s (Multiset.card s - k)
theorem Polynomial.coeff_eq_esymm_roots_of_card {R : Type u_1} [] [] {p : } (hroots : Multiset.card () = ) {k : } (h : ) :
= * (-1) ^ () *

Vieta's formula for the coefficients and the roots of a polynomial over an integral domain with as many roots as its degree.

theorem Polynomial.coeff_eq_esymm_roots_of_splits {F : Type u_2} [] {p : } (hsplit : ) {k : } (h : ) :
= * (-1) ^ () *

Vieta's formula for split polynomials over a field.

theorem MvPolynomial.prod_C_add_X_eq_sum_esymm (R : Type u_1) (σ : Type u_2) [] [] :
(Finset.prod Finset.univ fun (i : σ) => Polynomial.X + Polynomial.C ()) = Finset.sum (Finset.range ()) fun (j : ) => Polynomial.C () * Polynomial.X ^ ()

A sum version of Vieta's formula for MvPolynomial: viewing X i as variables, the product of linear terms λ + X i is equal to a linear combination of the symmetric polynomials esymm σ R j.

theorem MvPolynomial.prod_X_add_C_coeff (R : Type u_1) (σ : Type u_2) [] [] (k : ) (h : ) :
Polynomial.coeff (Finset.prod Finset.univ fun (i : σ) => Polynomial.X + Polynomial.C ()) k = MvPolynomial.esymm σ R ()