mathlib documentation

ring_theory.polynomial.vieta

Vieta's Formula #

The main result is vieta.prod_X_add_C_eq_sum_esymm, which shows that the product of linear terms λ + X i is equal to a linear combination of the symmetric polynomials esymm σ R j.

Implementation Notes: #

We first take the viewpoint where the "roots" X i are variables. This means we work over polynomial (mv_polynomial σ R), which enables us to talk about linear combinations of esymm σ R j. We then derive Vieta's formula in polynomial R by giving a valuation from each X i to r i.

A sum version of Vieta's formula. 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_eval {R : Type u} [comm_semiring R] (σ : Type u) [fintype σ] (r : σ → R) :
∏ (i : σ), (polynomial.C (r i) + polynomial.X) = ∑ (i : ) in finset.range (fintype.card σ + 1), (∑ (t : finset σ) in finset.powerset_len i finset.univ, ∏ (i : σ) in t, polynomial.C (r i)) * polynomial.X ^ (fintype.card σ - i)

A fully expanded sum version of Vieta's formula, evaluated at the roots. The product of linear terms X + r i is equal to ∑ j in range (n + 1), e_j * X ^ (n - j), where e_j is the jth symmetric polynomial of the constant terms r i.

theorem mv_polynomial.esymm_to_sum {R : Type u} [comm_semiring R] (σ : Type u) [fintype σ] (r : σ → R) (j : ) :
theorem mv_polynomial.prod_X_add_C_coeff {R : Type u} [comm_semiring R] (σ : Type u) [fintype σ] (r : σ → R) (k : ) (h : k fintype.card σ) :
(∏ (i : σ), (polynomial.C (r i) + polynomial.X)).coeff k = ∑ (t : finset σ) in finset.powerset_len (fintype.card σ - k) finset.univ, ∏ (i : σ) in t, r i

Vieta's formula for the coefficients of the product of linear terms X + r i, The kth coefficient is ∑ t in powerset_len (card σ - k) (univ : finset σ), ∏ i in t, r i, i.e. the symmetric polynomial esymm σ R (card σ - k) of the constant terms r i.