English
The (m · n)-th Dickson polynomial of the first kind is the composition of the m-th and n-th: D_1,1(m n) = D_1,1(m) ∘ D_1,1(n).
Русский
Полином Диксона первого рода D_1,1(m n) равен композиции D_1,1(m) и D_1,1(n).
LaTeX
$$dickson\, 1\, (1 : R)\, (m * n) = (dickson\, 1\, 1\, m).comp (dickson\, 1\, 1\, n)$$
Lean4
/-- The `(m * n)`-th Dickson polynomial of the first kind is the composition of the `m`-th and
`n`-th. -/
theorem dickson_one_one_mul (m n : ℕ) : dickson 1 (1 : R) (m * n) = (dickson 1 1 m).comp (dickson 1 1 n) :=
by
have h : (1 : R) = Int.castRingHom R 1 := by simp only [eq_intCast, Int.cast_one]
rw [h]
simp only [← map_dickson (Int.castRingHom R), ← map_comp]
congr 1
apply map_injective (Int.castRingHom ℚ) Int.cast_injective
simp only [map_dickson, map_comp, eq_intCast, Int.cast_one, dickson_one_one_eq_chebyshev_T, Nat.cast_mul,
Chebyshev.T_mul, two_mul, ← add_comp]
simp only [← two_mul, ← comp_assoc]
apply eval₂_congr rfl rfl
rw [comp_assoc]
apply eval₂_congr rfl _ rfl
rw [mul_comp, C_comp, X_comp, ← mul_assoc, C_half_mul_two_eq_one, one_mul]
