case h
R : Type u_1
S : Type ?u.318902
inst✝³ : CommRing R
inst✝² : CommRing S
k : ℕ
a : R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
⊢ 1 = ↑(ZMod.castHom (_ : p ∣ p) R) 1

R : Type u_1
S : Type ?u.318902
inst✝³ : CommRing R
inst✝² : CommRing S
k : ℕ
a : R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
h : 1 = ↑(ZMod.castHom (_ : p ∣ p) R) 1
⊢ dickson 1 1 p = X ^ p
R : Type u_1
S : Type ?u.318902
inst✝³ : CommRing R
inst✝² : CommRing S
k : ℕ
a : R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
⊢ dickson 1 1 p = X ^ p
have h : (1 : R) = ZMod.castHom (dvd_refl p) R 1
R : Type u_1
S : Type ?u.318902
inst✝³ : CommRing R
inst✝² : CommRing S
k : ℕ
a : R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
h : 1 = ↑(ZMod.castHom (_ : p ∣ p) R) 1
⊢ dickson 1 1 p = X ^ p
case h
R : Type u_1
S : Type ?u.318902
inst✝³ : CommRing R
inst✝² : CommRing S
k : ℕ
a : R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
⊢ 1 = ↑(ZMod.castHom (_ : p ∣ p) R) 1

R : Type u_1
S : Type ?u.318902
inst✝³ : CommRing R
inst✝² : CommRing S
k : ℕ
a : R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
h : 1 = ↑(ZMod.castHom (_ : p ∣ p) R) 1
⊢ dickson 1 1 p = X ^ p
simp only [ZMod.castHom_apply, ZMod.cast_one']
no goals
R : Type u_1
S : Type ?u.318902
inst✝³ : CommRing R
inst✝² : CommRing S
k : ℕ
a : R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
h : 1 = ↑(ZMod.castHom (_ : p ∣ p) R) 1
⊢ dickson 1 1 p = X ^ p
rw [h, ← map_dickson (ZMod.castHom (dvd_refl p) R), dickson_one_one_zmod_p, Polynomial.map_pow,
  map_X]