no goals
R : Type u_1
S : Type ?u.69485
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (1 - X ^ 2) * ↑derivative (T R (n + 1)) = (1 - X ^ 2) * ((↑n + 1) * U R n)
rw [T_derivative_eq_U]
no goals
R : Type u_1
S : Type ?u.69485
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (1 - X ^ 2) * ((↑n + 1) * U R n) = (↑n + 1) * ((1 - X ^ 2) * U R n)
ring
no goals
R : Type u_1
S : Type ?u.69485
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 1) * ((1 - X ^ 2) * U R n) = (↑n + 1) * (X * T R (n + 1) - (2 * X * T R (n + 1) - T R n))
rw [one_sub_X_sq_mul_U_eq_pol_in_T, T_add_two]
no goals
R : Type u_1
S : Type ?u.69485
inst✝¹ : CommRing R
inst✝ : CommRing S
n : ℕ
⊢ (↑n + 1) * (X * T R (n + 1) - (2 * X * T R (n + 1) - T R n)) = (↑n + 1) * (T R n - X * T R (n + 1))
ring