Polynomials and power series
Univariate and multivariate polynomials and formal power series as algebraic objects: coefficients, derivations, symmetric polynomials, irreducibility, polynomial maps and rational series.
- Alternating binomial sums of rational functions
- Binomial convolutions of rational power series
- Coefficient L1 norm of multivariate polynomials
- Coefficients of products with linear factors
- Deep power-sum congruences
- Denominators of rational polynomials
- Irreducibility criteria for integer polynomials
- Mestre's square decomposition
- Mixed partial derivatives of polynomials
- Newton polygon
- Partial fraction decomposition
- Polynomial automorphisms of the plane
- Polynomial maps between affine spaces
- Polynomials with coefficients in arithmetic progression
- Reciprocal 0,1-polynomials
- Squares of sparse polynomials
- Weighted derivations of monoid algebras
TheoremSymmetric polynomials in the roots are polynomials in the coefficients#✓fully proved
A symmetric polynomial is a polynomial in the elementary symmetric
polynomials, with a single witness q depending only on f; consequently,
for every monic split polynomial P, that same q evaluated at the signed
coefficients of P equals f evaluated at the roots of P. This is the
book's corollary that a symmetric polynomial in the roots of P can be
written as a polynomial in the coefficients of P; the signed coefficients
are the elementary symmetric polynomials in the roots, by Vieta's formulas.
theorem symmetric_polynomial_in_esymm
{F : Type*} [Field F] {n : ℕ}
(f : MvPolynomial (Fin n) F) (hf : f.IsSymmetric) :
∃ q : MvPolynomial (Fin n) F,
f = MvPolynomial.aeval
(fun i : Fin n => MvPolynomial.esymm (Fin n) F (i.val + 1)) q ∧
∀ {P : Polynomial F} {α : Fin n → F},
P = ∏ i : Fin n, (Polynomial.X - Polynomial.C (α i)) →
MvPolynomial.eval α f =
MvPolynomial.eval
(fun i : Fin n => (-1 : F) ^ (i.val + 1) * P.coeff (n - (i.val + 1))) qLoading dependency explorer…
The dependency explorer needs JavaScript and its graph data.