# mathlib3documentation

ring_theory.polynomial.dickson

# Dickson polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 parameter 1 : R is the composition of the m-th and n-th Dickson polynomials of the first kind for 1 : R.
• polynomial.dickson_one_one_char_p, for a prime number p, the p-th Dickson polynomial of the first kind associated to parameter 1 : R is congruent to X ^ p modulo p.

## TODO #

• Redefine dickson in terms of linear_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.
noncomputable def polynomial.dickson {R : Type u_1} [comm_ring R] (k : ) (a : R) :

dickson is the nthe (generalised) Dickson polynomial of the k-th kind associated to the element a ∈ R.

Equations
@[simp]
theorem polynomial.dickson_zero {R : Type u_1} [comm_ring R] (k : ) (a : R) :
0 = 3 - k
@[simp]
theorem polynomial.dickson_one {R : Type u_1} [comm_ring R] (k : ) (a : R) :
theorem polynomial.dickson_two {R : Type u_1} [comm_ring R] (k : ) (a : R) :
2 = - * (3 - k)
@[simp]
theorem polynomial.dickson_add_two {R : Type u_1} [comm_ring R] (k : ) (a : R) (n : ) :
(n + 2) = polynomial.X * (n + 1) - * n
theorem polynomial.dickson_of_two_le {R : Type u_1} [comm_ring R] (k : ) (a : R) {n : } (h : 2 n) :
n = polynomial.X * (n - 1) - * (n - 2)
theorem polynomial.map_dickson {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {k : } {a : R} (f : R →+* S) (n : ) :
n) = (f a) n
@[simp]
theorem polynomial.dickson_two_zero {R : Type u_1} [comm_ring R] (n : ) :
n =

### A Lambda structure on ℤ[X]#

Mathlib doesn't currently know what a Lambda ring is. But once it does, we can endow ℤ[X] with a Lambda structure in terms of the dickson 1 1 polynomials defined below. There is exactly one other Lambda structure on ℤ[X] in terms of binomial polynomials.

theorem polynomial.dickson_one_one_eval_add_inv {R : Type u_1} [comm_ring R] (x y : R) (h : x * y = 1) (n : ) :
polynomial.eval (x + y) n) = x ^ n + y ^ n
theorem polynomial.dickson_one_one_mul (R : Type u_1) [comm_ring R] (m n : ) :
(m * n) = m).comp n)

The (m * n)-th Dickson polynomial of the first kind is the composition of the m-th and n-th.

theorem polynomial.dickson_one_one_comp_comm (R : Type u_1) [comm_ring R] (m n : ) :
m).comp n) = n).comp m)
theorem polynomial.dickson_one_one_char_p (R : Type u_1) [comm_ring R] (p : ) [fact (nat.prime p)] [ p] :
p =