Dickson polynomials #
The (generalised) Dickson polynomials are a family of polynomials indexed by ℕ × ℕ
,
with coefficients in a commutative ring R
depending on an element a∈R
. More precisely, the
they satisfy the recursion dickson k a (n + 2) = X * (dickson k a n + 1) - a * (dickson k a n)
with starting values dickson k a 0 = 3 - k
and dickson k a 1 = X
. In the literature,
dickson k a n
is called the n
-th Dickson polynomial of the k
-th kind associated to the
parameter a : R
. They are closely related to the Chebyshev polynomials in the case that a=1
.
When a=0
they are just the family of monomials X ^ n
.
Main definition #
polynomial.dickson
: the generalised Dickson polynomials.
Main statements #
polynomial.dickson_one_one_mul
, the(m * n)
-th Dickson polynomial of the first kind for parameter1 : R
is the composition of them
-th andn
-th Dickson polynomials of the first kind for1 : R
.polynomial.dickson_one_one_char_p
, for a prime numberp
, thep
-th Dickson polynomial of the first kind associated to parameter1 : R
is congruent toX ^ p
modulop
.
References #
TODO #
- Redefine
dickson
in terms oflinear_recurrence
. - Show that
dickson 2 1
is equal to the characteristic polynomial of the adjacency matrix of a type A Dynkin diagram. - Prove that the adjacency matrices of simply laced Dynkin diagrams are precisely the adjacency
matrices of simple connected graphs which annihilate
dickson 2 1
.
dickson
is the n
the (generalised) Dickson polynomial of the k
-th kind associated to the
element a ∈ R
.
Equations
- polynomial.dickson k a (n + 2) = polynomial.X * polynomial.dickson k a n.succ - ⇑polynomial.C a * polynomial.dickson k a n
- polynomial.dickson k a 1 = polynomial.X
- polynomial.dickson k a 0 = 3 - ↑k
A Lambda structure on polynomial ℤ
#
Mathlib doesn't currently know what a Lambda ring is.
But once it does, we can endow polynomial ℤ
with a Lambda structure
in terms of the dickson 1 1
polynomials defined below.
There is exactly one other Lambda structure on polynomial ℤ
in terms of binomial polynomials.
The (m * n)
-th Dickson polynomial of the first kind is the composition of the m
-th and
n
-th.