mathlibdocumentation

ring_theory.polynomial.vieta

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

theorem multiset.prod_X_add_C_eq_sum_esymm {R : Type u_1} (s : multiset R) :
(multiset.map (λ (r : R), s).prod = (finset.range + 1)).sum (λ (j : ), polynomial.C (s.esymm j) * polynomial.X ^ - 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 : multiset R) {k : } (h : k ) :
(multiset.map (λ (r : R), s).prod.coeff k = s.esymm - 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.esymm_neg {R : Type u_1} [comm_ring R] (s : multiset R) (k : ) :
k = (-1) ^ k * s.esymm k
theorem multiset.prod_X_sub_C_eq_sum_esymm {R : Type u_1} [comm_ring R] (s : multiset R) :
(multiset.map (λ (t : R), s).prod = (finset.range + 1)).sum (λ (j : ), (-1) ^ j * (polynomial.C (s.esymm j) * polynomial.X ^ - j)))
theorem multiset.prod_X_sub_C_coeff {R : Type u_1} [comm_ring R] (s : multiset R) {k : } (h : k ) :
(multiset.map (λ (t : R), s).prod.coeff k = (-1) ^ - k) * s.esymm - k)
theorem polynomial.coeff_eq_esymm_roots_of_card {R : Type u_1} [comm_ring R] [is_domain R] {p : polynomial R} (hroots : = 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.

theorem polynomial.coeff_eq_esymm_roots_of_splits {F : Type u_1} [field F] {p : polynomial F} (hsplit : 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.

theorem mv_polynomial.prod_C_add_X_eq_sum_esymm (R : Type u_1) (σ : Type u_2) [fintype σ] :
finset.univ.prod (λ (i : σ), = (finset.range + 1)).sum (λ (j : ), polynomial.C j) * polynomial.X ^ - 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.

theorem mv_polynomial.prod_X_add_C_coeff (R : Type u_1) (σ : Type u_2) [fintype σ] (k : ) (h : k ) :
(finset.univ.prod (λ (i : σ), .coeff k = - k)