### Abstract

This article provides a formalisation of the symmetric multivariate polynomials known as power sum polynomials. These are of the form pn(X1,…, Xk) = X1n + … + Xkn. A formal proof of the Girard–Newton Theorem is also given. This theorem relates the power sum polynomials to the elementary symmetric polynomials sk in the form of a recurrence relation (-1)k k sk = ∑i∈[0,k) (-1)i si pk-i.

As an application, this is then used to solve a generalised form of a puzzle given as an exercise in Dummit and Foote's Abstract Algebra: For k complex unknowns x1, …, xk, define pj := x1j + … + xkj. Then for each vector a ∈ ℂk, show that there is exactly one solution to the system p1 = a1, …, pk = ak up to permutation of the xi and determine the value of pi for i>k.

### License

BSD License

### Topics

- Mathematics/Algebra

### Session Power_Sum_Polynomials

- Power_Sum_Polynomials_Library
- Power_Sum_Polynomials
- Power_Sum_Puzzle

### Depends on

- Polynomial Factorization
- Symmetric Polynomials

### Used by

- The Hermite–Lindemann–Weierstraß Transcendence Theorem

### Auto-related entries

- A Case Study in Basic Algebra

## Cite

×

Power_Sum_Polynomials-AFP

    @article{Power_Sum_Polynomials-AFP,
      author  = {Manuel Eberl},
      title   = {Power Sum Polynomials},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Power_Sum_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 30, 2020 : Isabelle2020