Power Sum Polynomials

This article provides a formalisation of the symmetric multivariate polynomials known as power sum polynomials. These are of the form p_n(X₁,…, X_k) = X₁ⁿ + … + X_kⁿ. A formal proof of the Girard–Newton Theorem is also given. This theorem relates the power sum polynomials to the elementary symmetric polynomials s_k in the form of a recurrence relation (-1)^k k s_k = ∑_i∈[0,k) (-1)ⁱ s_i p_k-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 x₁, …, x_k, define p_j := x₁^j + … + x_k^j. Then for each vector a ∈ ℂ^k, show that there is exactly one solution to the system p₁ = a₁, …, p_k = a_k up to permutation of the x_i and determine the value of p_i for i>k.