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} [CommSemiring R] (s : Multiset R) : (Multiset.map (fun (r : R) => Polynomial.X + Polynomial.C r) s).prod = ∑ j ∈ Finset.range (s.card + 1), Polynomial.C (s.esymm j) * Polynomial.X ^ (s.card - 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} [CommSemiring R] (s : Multiset R) {k : ℕ} (h : k ≤ s.card) : (Multiset.map (fun (r : R) => Polynomial.X + Polynomial.C r) s).prod.coeff k = s.esymm (s.card - 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} [CommSemiring R] {σ : Type u_2} (s : Multiset σ) (r : σ → R) {k : ℕ} (h : k ≤ s.card) : (Multiset.map (fun (i : σ) => Polynomial.X + Polynomial.C (r i)) s).prod.coeff k = (Multiset.map r s).esymm (s.card - k)

theorem Finset.prod_X_add_C_coeff {R : Type u_1} [CommSemiring R] {σ : Type u_2} (s : Finset σ) (r : σ → R) {k : ℕ} (h : k ≤ s.card) : (∏ i ∈ s, (Polynomial.X + Polynomial.C (r i))).coeff k = ∑ t ∈ Finset.powersetCard (s.card - k) s, ∏ i ∈ t, r i

theorem Multiset.esymm_neg {R : Type u_1} [CommRing R] (s : Multiset R) (k : ℕ) : (Multiset.map Neg.neg s).esymm k = (-1) ^ k * s.esymm k

theorem Multiset.prod_X_sub_X_eq_sum_esymm {R : Type u_1} [CommRing R] (s : Multiset R) : (Multiset.map (fun (t : R) => Polynomial.X - Polynomial.C t) s).prod = ∑ j ∈ Finset.range (s.card + 1), (-1) ^ j * (Polynomial.C (s.esymm j) * Polynomial.X ^ (s.card - j))

theorem Multiset.prod_X_sub_C_coeff {R : Type u_1} [CommRing R] (s : Multiset R) {k : ℕ} (h : k ≤ s.card) : (Multiset.map (fun (t : R) => Polynomial.X - Polynomial.C t) s).prod.coeff k = (-1) ^ (s.card - k) * s.esymm (s.card - k)

theorem Polynomial.coeff_eq_esymm_roots_of_card {R : Type u_1} [CommRing R] [IsDomain R] {p : Polynomial R} (hroots : p.roots.card = p.natDegree) {k : ℕ} (h : k ≤ p.natDegree) : p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

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} [Field F] {p : Polynomial F} (hsplit : Polynomial.Splits (RingHom.id F) p) {k : ℕ} (h : k ≤ p.natDegree) : p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

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) [CommSemiring R] [Fintype σ] : ∏ i : σ, (Polynomial.X + Polynomial.C (MvPolynomial.X i)) = ∑ j ∈ Finset.range (Fintype.card σ + 1), Polynomial.C (MvPolynomial.esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)

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) [CommSemiring R] [Fintype σ] (k : ℕ) (h : k ≤ Fintype.card σ) : (∏ i : σ, (Polynomial.X + Polynomial.C (MvPolynomial.X i))).coeff k = MvPolynomial.esymm σ R (Fintype.card σ - k)