R : Type u_1
S : Type ?u.173812
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
⊢ 3 - ↑1 = 2
R : Type u_1
S : Type ?u.173812
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
⊢ dickson 1 1 0 = 2 * comp (Chebyshev.T R 0) (↑C ⅟2 * X)
simp only [Chebyshev.T_zero, mul_one, one_comp, dickson_zero]
no goals
R : Type u_1
S : Type ?u.173812
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
⊢ 3 - ↑1 = 2
norm_num
no goals
R : Type u_1
S : Type ?u.173812
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
⊢ dickson 1 1 1 = 2 * comp (Chebyshev.T R 1) (↑C ⅟2 * X)
rw [dickson_one, Chebyshev.T_one, X_comp, ← mul_assoc, two_mul_C_half_eq_one, one_mul]
R : Type u_1
S : Type ?u.173812
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
n : ℕ
⊢ X * (2 * comp (Chebyshev.T R (n + 1)) (↑C ⅟2 * X)) - 1 * (2 * comp (Chebyshev.T R n) (↑C ⅟2 * X)) =
    2 * (↑2 * (↑C ⅟2 * X) * comp (Chebyshev.T R (n + 1)) (↑C ⅟2 * X) - comp (Chebyshev.T R n) (↑C ⅟2 * X))
R : Type u_1
S : Type ?u.173812
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
n : ℕ
⊢ dickson 1 1 (n + 2) = 2 * comp (Chebyshev.T R (n + 2)) (↑C ⅟2 * X)
rw [dickson_add_two, C_1, Chebyshev.T_add_two, dickson_one_one_eq_chebyshev_T (n + 1),
  dickson_one_one_eq_chebyshev_T n, sub_comp, mul_comp, mul_comp, X_comp, ofNat_comp]
R : Type u_1
S : Type ?u.173812
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
n : ℕ
⊢ X * 2 * comp (Chebyshev.T R (n + 1)) (↑C ⅟2 * X) - 1 * 2 * comp (Chebyshev.T R n) (↑C ⅟2 * X) =
    2 * (1 * X * comp (Chebyshev.T R (n + 1)) (↑C ⅟2 * X) - comp (Chebyshev.T R n) (↑C ⅟2 * X))
R : Type u_1
S : Type ?u.173812
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
n : ℕ
⊢ X * (2 * comp (Chebyshev.T R (n + 1)) (↑C ⅟2 * X)) - 1 * (2 * comp (Chebyshev.T R n) (↑C ⅟2 * X)) =
    2 * (↑2 * (↑C ⅟2 * X) * comp (Chebyshev.T R (n + 1)) (↑C ⅟2 * X) - comp (Chebyshev.T R n) (↑C ⅟2 * X))
simp_rw [← mul_assoc, Nat.cast_ofNat, two_mul_C_half_eq_one]
no goals
R : Type u_1
S : Type ?u.173812
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
n : ℕ
⊢ X * 2 * comp (Chebyshev.T R (n + 1)) (↑C ⅟2 * X) - 1 * 2 * comp (Chebyshev.T R n) (↑C ⅟2 * X) =
    2 * (1 * X * comp (Chebyshev.T R (n + 1)) (↑C ⅟2 * X) - comp (Chebyshev.T R n) (↑C ⅟2 * X))
ring