Vieta's Formula #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 mv_polynomial.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).

source

theorem multiset.prod_X_add_C_eq_sum_esymm {R : Type u_1} [comm_semiring R] (s : multiset R) :

(multiset.map (λ (r : R), polynomial.X + ⇑polynomial.C r) s).prod = (finset.range (⇑multiset.card s + 1)).sum (λ (j : ℕ), ⇑polynomial.C (s.esymm j) * 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 .

source

theorem multiset.prod_X_add_C_coeff {R : Type u_1} [comm_semiring R] (s : multiset R) {k : ℕ} (h : k ≤ ⇑multiset.card s) :

(multiset.map (λ (r : R), polynomial.X + ⇑polynomial.C r) s).prod.coeff k = s.esymm (⇑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.

source

theorem multiset.prod_X_add_C_coeff' {R : Type u_1} [comm_semiring R] {σ : Type u_2} (s : multiset σ) (r : σ → R) {k : ℕ} (h : k ≤ ⇑multiset.card s) :

(multiset.map (λ (i : σ), polynomial.X + ⇑polynomial.C (r i)) s).prod.coeff k = (multiset.map r s).esymm (⇑multiset.card s - k)

source

theorem finset.prod_X_add_C_coeff {R : Type u_1} [comm_semiring R] {σ : Type u_2} (s : finset σ) (r : σ → R) {k : ℕ} (h : k ≤ s.card) :

(s.prod (λ (i : σ), polynomial.X + ⇑polynomial.C (r i))).coeff k = (finset.powerset_len (s.card - k) s).sum (λ (t : finset σ), t.prod (λ (i : σ), r i))

source

theorem multiset.esymm_neg {R : Type u_1} [comm_ring R] (s : multiset R) (k : ℕ) :

(multiset.map has_neg.neg s).esymm k = (-1) ^ k * s.esymm k

source

theorem multiset.prod_X_sub_C_eq_sum_esymm {R : Type u_1} [comm_ring R] (s : multiset R) :

(multiset.map (λ (t : R), polynomial.X - ⇑polynomial.C t) s).prod = (finset.range (⇑multiset.card s + 1)).sum (λ (j : ℕ), (-1) ^ j * (⇑polynomial.C (s.esymm j) * polynomial.X ^ (⇑multiset.card s - j)))

source

theorem multiset.prod_X_sub_C_coeff {R : Type u_1} [comm_ring R] (s : multiset R) {k : ℕ} (h : k ≤ ⇑multiset.card s) :

(multiset.map (λ (t : R), polynomial.X - ⇑polynomial.C t) s).prod.coeff k = (-1) ^ (⇑multiset.card s - k) * s.esymm (⇑multiset.card s - k)

source

theorem polynomial.coeff_eq_esymm_roots_of_card {R : Type u_1} [comm_ring R] [is_domain R] {p : polynomial R} (hroots : ⇑multiset.card p.roots = p.nat_degree) {k : ℕ} (h : k ≤ p.nat_degree) :

p.coeff k = p.leading_coeff * (-1) ^ (p.nat_degree - k) * p.roots.esymm (p.nat_degree - k)

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

source

theorem polynomial.coeff_eq_esymm_roots_of_splits {F : Type u_1} [field F] {p : polynomial F} (hsplit : polynomial.splits (ring_hom.id F) p) {k : ℕ} (h : k ≤ p.nat_degree) :

p.coeff k = p.leading_coeff * (-1) ^ (p.nat_degree - k) * p.roots.esymm (p.nat_degree - k)

Vieta's formula for split polynomials over a field.

source

theorem mv_polynomial.prod_C_add_X_eq_sum_esymm (R : Type u_1) (σ : Type u_2) [comm_semiring R] [fintype σ] :

finset.univ.prod (λ (i : σ), polynomial.X + ⇑polynomial.C (mv_polynomial.X i)) = (finset.range (fintype.card σ + 1)).sum (λ (j : ℕ), ⇑polynomial.C (mv_polynomial.esymm σ R j) * polynomial.X ^ (fintype.card σ - j))

A sum version of Vieta's formula for mv_polynomial: 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.

source

theorem mv_polynomial.prod_X_add_C_coeff (R : Type u_1) (σ : Type u_2) [comm_semiring R] [fintype σ] (k : ℕ) (h : k ≤ fintype.card σ) :

(finset.univ.prod (λ (i : σ), polynomial.X + ⇑polynomial.C (mv_polynomial.X i))).coeff k = mv_polynomial.esymm σ R (fintype.card σ - k)