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},
}
|