# mathlibdocumentation

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.

theorem mv_polynomial.prod_X_add_C_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. 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_1} (σ : Type u_2) [fintype σ] (r : σ → R) :
finset.univ.prod (λ (i : σ), polynomial.C (r i) + polynomial.X) = (finset.range + 1)).sum (λ (i : ), (λ (t : finset σ), t.prod (λ (i : σ), polynomial.C (r i))) * polynomial.X ^ - 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_1} (σ : Type u_2) [fintype σ] (r : σ → R) (j : ) :
polynomial.C ( j)) = (λ (t : finset σ), t.prod (λ (i : σ), polynomial.C (r i)))
theorem mv_polynomial.prod_X_add_C_coeff {R : Type u_1} (σ : Type u_2) [fintype σ] (r : σ → R) (k : ) (h : k ) :
(finset.univ.prod (λ (i : σ), polynomial.C (r i) + polynomial.X)).coeff k = .sum (λ (t : finset σ), t.prod (λ (i : σ), 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.