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 j
th symmetric polynomial of the constant terms r i
.
Vieta's formula for the coefficients of the product of linear terms X + r i
,
The k
th 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
.