English
For a commutative ring R with elements k and a ∈ R, there is a well-defined sequence of polynomials D_n ∈ R[X] (n ∈ N) given by D_0 = 3 − k, D_1 = X, and D_{n+2} = X D_{n+1} − C_a D_n, where C_a is the constant polynomial a.
Русский
Для коммутативного кольца R и элементов k и a ∈ R существует последовательность полиномов D_n ∈ R[X] (n ∈ N), определяемая как D_0 = 3 − k, D_1 = X, и D_{n+2} = X D_{n+1} − C_a D_n, где C_a — константный полином, равный a.
LaTeX
$$$dickson : \mathbb{N} \to R[X],\quad
dickson\, 0\, a = 3 - k,\; dickson\, 1\, a = X,\; dickson\, (n+2)\, a = X \cdot dickson\, (n+1)\, a - C\, a \cdot dickson\, n\, a$$$
Lean4
/-- `dickson` is the `n`-th (generalised) Dickson polynomial of the `k`-th kind associated to the
element `a ∈ R`. -/
noncomputable def dickson : ℕ → R[X]
| 0 => 3 - k
| 1 => X
| n + 2 => X * dickson (n + 1) - C a * dickson n
