Polynomial.dickson_one_one_mul

theorem Polynomial.dickson_one_one_mul : ∀ (R : Type u_1) [inst : CommRing R] (m n : ℕ), Polynomial.dickson 1 1 (m * n) = (Polynomial.dickson 1 1 m).comp (Polynomial.dickson 1 1 n)

This theorem states that for any commutative ring `R`, the `(m * n)`-th Dickson polynomial of the first kind, associated to the element `1` in `R`, is equal to the composition of the `m`-th and `n`-th Dickson polynomials of the first kind, both also associated to the element `1` in `R`. The Dickson polynomial of the first kind is a special case of the generalized Dickson polynomial when `k` is `1`.

More concisely: For any commutative ring R, the (m * n)-th Dickson polynomial of the first kind associated to 1 is equal to the composition of the m-th and n-th Dickson polynomials of the first kind, both associated to 1. In other words, D_m(D_n(1)) = D_{m*n}(1).