R : Type u_1
S : Type ?u.114565
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
⊢ 3 - ↑2 = 1
R : Type u_1
S : Type ?u.114565
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
⊢ dickson 2 0 0 = X ^ 0
simp only [dickson_zero, pow_zero]
no goals
R : Type u_1
S : Type ?u.114565
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
⊢ 3 - ↑2 = 1
norm_num
no goals
R : Type u_1
S : Type ?u.114565
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
⊢ dickson 2 0 1 = X ^ 1
simp only [dickson_one, pow_one]
R : Type u_1
S : Type ?u.114565
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
n : ℕ
⊢ X * dickson 2 0 (n + 1) = X ^ (n + 2)
R : Type u_1
S : Type ?u.114565
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
n : ℕ
⊢ dickson 2 0 (n + 2) = X ^ (n + 2)
simp only [dickson_add_two, C_0, MulZeroClass.zero_mul, sub_zero]
no goals
R : Type u_1
S : Type ?u.114565
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
n : ℕ
⊢ X * dickson 2 0 (n + 1) = X ^ (n + 2)
rw [dickson_two_zero (n + 1), pow_add X (n + 1) 1, mul_comm, pow_one]