# Power Sum Polynomials

 Title: Power Sum Polynomials Author: Manuel Eberl Submission date: 2020-04-24 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. BibTeX: @article{Power_Sum_Polynomials-AFP, author = {Manuel Eberl}, title = {Power Sum Polynomials}, journal = {Archive of Formal Proofs}, month = apr, year = 2020, note = {\url{http://isa-afp.org/entries/Power_Sum_Polynomials.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Polynomial_Factorization, Symmetric_Polynomials Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.