mathlib3 documentation

ring_theory.polynomial.vieta

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

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 .

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