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