no goals
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
⊢ map f (dickson k a 0) = dickson k (↑f a) 0
simp_rw [dickson_zero, Polynomial.map_sub, Polynomial.map_nat_cast, Polynomial.map_ofNat]
no goals
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
⊢ map f (dickson k a 1) = dickson k (↑f a) 1
simp only [dickson_one, map_X]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
n : ℕ
⊢ X * map f (dickson k a (n + 1)) - ↑C (↑f a) * map f (dickson k a n) =
    X * dickson k (↑f a) (n + 1) - ↑C (↑f a) * dickson k (↑f a) n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
n : ℕ
⊢ map f (dickson k a (n + 2)) = dickson k (↑f a) (n + 2)
simp only [dickson_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, map_C]
no goals
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
n : ℕ
⊢ X * map f (dickson k a (n + 1)) - ↑C (↑f a) * map f (dickson k a n) =
    X * dickson k (↑f a) (n + 1) - ↑C (↑f a) * dickson k (↑f a) n
rw [map_dickson f n, map_dickson f (n + 1)]