R : Type u_1
S : Type ?u.201283
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
n : ℕ
⊢ Chebyshev.T R n = ↑C ⅟2 * (↑2 * comp (Chebyshev.T R n) (↑C ⅟2 * (2 * X)))
R : Type u_1
S : Type ?u.201283
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
n : ℕ
⊢ Chebyshev.T R n = ↑C ⅟2 * comp (dickson 1 1 n) (2 * X)
rw [dickson_one_one_eq_chebyshev_T, mul_comp, ofNat_comp, comp_assoc, mul_comp, C_comp, X_comp]
no goals
R : Type u_1
S : Type ?u.201283
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
n : ℕ
⊢ Chebyshev.T R n = ↑C ⅟2 * (↑2 * comp (Chebyshev.T R n) (↑C ⅟2 * (2 * X)))
simp_rw [← mul_assoc, Nat.cast_ofNat, C_half_mul_two_eq_one, one_mul, comp_X]