### Abstract

A symmetric polynomial is a polynomial in variables X1,…,Xn that does not discriminate between its variables, i. e. it is invariant under any permutation of them. These polynomials are important in the study of the relationship between the coefficients of a univariate polynomial and its roots in its algebraic closure.

This article provides a definition of symmetric polynomials and the elementary symmetric polynomials e1,…,en and proofs of their basic properties, including three notable ones:

- Vieta's formula, which gives an explicit expression for the k-th coefficient of a univariate monic polynomial in terms of its roots x1,…,xn, namely ck = (-1)n-ken-k(x1,…,xn).
- Second, the Fundamental Theorem of Symmetric Polynomials, which states that any symmetric polynomial is itself a uniquely determined polynomial combination of the elementary symmetric polynomials.
- Third, as a corollary of the previous two, that given a polynomial over some ring R, any symmetric polynomial combination of its roots is also in R even when the roots are not.

Both the symmetry property itself and the witness for the Fundamental Theorem are executable.

### License

BSD License

### Topics

- Mathematics/Algebra

### Session Symmetric_Polynomials

- Vieta
- Symmetric_Polynomials
- Symmetric_Polynomials_Code

### Depends on

- Executable Multivariate Polynomials

### Used by

- Power Sum Polynomials
- The Transcendence of π

### Auto-related entries

- The Theorem of Three Circles

## Cite

×

Symmetric_Polynomials-AFP

    @article{Symmetric_Polynomials-AFP,
      author  = {Manuel Eberl},
      title   = {Symmetric Polynomials},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Symmetric_Polynomials.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Sep 26, 2018 : Isabelle2018