mathlib documentation

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

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} [comm_semiring R] (s : multiset R) {k : } (h : k multiset.card s) :

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 : ) :
theorem multiset.prod_X_sub_C_coeff {R : Type u_1} [comm_ring R] (s : multiset R) {k : } (h : k multiset.card s) :
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.

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.

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) [comm_semiring R] [fintype σ] (k : ) (h : k fintype.card σ) :