Polynomial.coeff_eq_esymm_roots_of_card
theorem Polynomial.coeff_eq_esymm_roots_of_card :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
Multiset.card p.roots = p.natDegree →
∀ {k : ℕ},
k ≤ p.natDegree → p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
This theorem is a statement of Vieta's formula for the coefficients and the roots of a polynomial over an integral domain. It asserts that for any polynomial `p` over a commutative ring `R` that is also an integral domain, if the cardinality of the roots of the polynomial equals its degree, then for any non-negative integer `k` that is less than or equal to the degree of the polynomial, the `k`-th coefficient of the polynomial is equal to the leading coefficient of the polynomial times `(-1)` to the power of the difference of the degree and `k`, times the `esymm` (elementary symmetric function) of the roots of the polynomial of the same order.
More concisely: For a polynomial `p` of degree `n` over a commutative integral domain `R` with exactly `n` distinct roots, the `k`-th coefficient of `p` is equal to the leading coefficient of `p` multiplied by `(-1)` raised to the power of `n-k` and by the `k`-th elementary symmetric function of the polynomial's roots.
|
MvPolynomial.prod_C_add_X_eq_sum_esymm
theorem MvPolynomial.prod_C_add_X_eq_sum_esymm :
∀ (R : Type u_1) (σ : Type u_2) [inst : CommSemiring R] [inst_1 : Fintype σ],
(Finset.univ.prod fun i => Polynomial.X + Polynomial.C (MvPolynomial.X i)) =
(Finset.range (Fintype.card σ + 1)).sum fun j =>
Polynomial.C (MvPolynomial.esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
This theorem is a sum version of Vieta's formula in the context of multivariate polynomials (`MvPolynomial`). Given a commutative semiring `R` and a fintype `σ`, it states that the product of linear polynomials of the form `λ + X i` for every `i` in the universal set (`Finset.univ`), where `λ` is the polynomial variable and `X i` are the variables of the multivariate polynomial, is equal to a sum of terms. Each term in the sum is a product of a constant polynomial `C` whose value is the `j`th elementary symmetric polynomial (`esymm σ R j`), and `X` raised to the power of `σ`'s cardinality minus `j`. The summation runs through all natural numbers less than `σ`'s cardinality plus one (`Finset.range (Fintype.card σ + 1)`).
More concisely: Given a commutative semiring R and a finite set σ, the product of linear polynomials in the multivariate polynomial over R with variables {λ, X i | i ∈ σ} equals the sum of terms, where each term is a constant times X raised to the power of |σ| - j, for j ranging from 0 to |σ|.
|
Multiset.prod_X_add_C_coeff
theorem Multiset.prod_X_add_C_coeff :
∀ {R : Type u_1} [inst : CommSemiring R] (s : Multiset R) {k : ℕ},
k ≤ Multiset.card s →
(Multiset.map (fun r => Polynomial.X + Polynomial.C r) s).prod.coeff k = s.esymm (Multiset.card s - k)
The theorem `Multiset.prod_X_add_C_coeff` is a formalization of Vieta's formula in Lean 4. It states that for any commutative semiring `R`, and for any multiset `s` of type `R`, the `k`th coefficient of the polynomial obtained by the product of linear terms `X + λ` where `λ` ranges over the elements in `s`, is equal to the symmetric function `esymm (card s - k) s` if `k` is less than or equal to the cardinality of `s`. Here, `Polynomial.X` represents the polynomial variable, `Polynomial.C r` is a constant polynomial `r`, and `esymm n s` is the `n`th elementary symmetric function. Vieta's formulas establish a clear relationship between the coefficients of a polynomial and the roots of the polynomial.
More concisely: For any commutative semiring R and multiset s of type R, the k-th coefficient of the polynomial product of X + λ over λ in s equals the (cardinality of s - k)-th elementary symmetric function of s, provided that k is less than or equal to the cardinality of s.
|
Multiset.prod_X_add_C_eq_sum_esymm
theorem Multiset.prod_X_add_C_eq_sum_esymm :
∀ {R : Type u_1} [inst : CommSemiring R] (s : Multiset R),
(Multiset.map (fun r => Polynomial.X + Polynomial.C r) s).prod =
(Finset.range (Multiset.card s + 1)).sum fun j =>
Polynomial.C (s.esymm j) * Polynomial.X ^ (Multiset.card s - j)
This is a multiset version of Vieta's formula in polynomial theory. The theorem states that for any commutative semiring `R` and a multiset `s` of `R`, the product of the linear terms `X + λ` where `λ` runs through the multiset `s` is equal to a sum of terms, where each term is a symmetric function `esymm` of the `λ`s multiplied by `X` to the power of the difference between the cardinality of the multiset `s` and the index. The sum is taken over the range from zero up to the cardinality of the multiset `s`.
More concisely: For any commutative semiring R and a multiset s of R, the product of X raised to the power of the difference between the cardinality of s and the index, and the symmetric function esymm of the elements in s, summed from i = 0 to the cardinality of s, equals the product of 1 + X*λ for all λ in s.
|
Polynomial.coeff_eq_esymm_roots_of_splits
theorem Polynomial.coeff_eq_esymm_roots_of_splits :
∀ {F : Type u_2} [inst : Field F] {p : Polynomial F},
Polynomial.Splits (RingHom.id F) p →
∀ {k : ℕ},
k ≤ p.natDegree → p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
This is Vieta's formula for split polynomials over a field. The theorem states that for any field F and polynomial p over F, if p splits over F (meaning that it is either the zero polynomial or all of its irreducible factors have degree 1), then for any natural number k that is less than or equal to the degree of the polynomial, the k-th coefficient of the polynomial equals the leading coefficient of the polynomial multiplied by (-1) raised to the power of the degree of the polynomial minus k, and further multiplied by the elementary symmetric function of the roots of the polynomial of order equal to the degree of the polynomial minus k. Here, the elementary symmetric function of a set of numbers is the sum of the products of the numbers taken k at a time.
More concisely: For any field F and polynomial p of degree n over F that splits over F, the k-th coefficient of p is equal to the leading coefficient of p times (-1)^(n-k) multiplied by the elementary symmetric function of the roots of p of degree n-k.
|