English
Let f be a ring hom R → S. Then mapping the Dickson polynomial via f commutes with the Dickson polynomial of the mapped coefficient: map f (dickson k a n) = dickson k (f a) n.
Русский
Пусть f: R → S — кольцо-функтор. Тогда отображение полинома Диксона через f совпадает с полиномом Диксона с образом коэффициента: map f(dickson k a n) = dickson k (f a) n.
LaTeX
$$map f (dickson k a n) = dickson k (RingHom.instFunLike.coe f a) n$$
Lean4
theorem map_dickson (f : R →+* S) : ∀ n : ℕ, map f (dickson k a n) = dickson k (f a) n
| 0 => by simp_rw [dickson_zero, Polynomial.map_sub, Polynomial.map_natCast, Polynomial.map_ofNat]
| 1 => by simp only [dickson_one, map_X]
| n + 2 => by
simp only [dickson_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, map_C]
rw [map_dickson f n, map_dickson f (n + 1)]
