English
For every integer n, the first-kind Chebyshev polynomial T_n equals U_n minus X times U_{n-1}.
Русский
Для каждого целого n полином Чебышёва первого рода T_n равен U_n минус X умноженное на U_{n-1}.
LaTeX
$$$ T(n) = U(n) - X\,U(n-1) $$$
Lean4
theorem U_eq_X_mul_U_add_T (n : ℤ) : U R (n + 1) = X * U R n + T R (n + 1) := by
induction n using Polynomial.Chebyshev.induct with
| zero => simp [two_mul]
| one => simp [U_two, T_two]; ring
| add_two n ih1 ih2 =>
have h₁ := U_add_two R (n + 1)
have h₂ := U_add_two R n
have h₃ := T_add_two R (n + 1)
linear_combination (norm := ring_nf) -h₃ - (X : R[X]) * h₂ + h₁ + 2 * (X : R[X]) * ih1 - ih2
| neg_add_one n ih1 ih2 =>
have h₁ := U_add_two R (-n - 1)
have h₂ := U_add_two R (-n)
have h₃ := T_add_two R (-n)
linear_combination (norm := ring_nf) -h₃ + h₂ - (X : R[X]) * h₁ - ih2 + 2 * (X : R[X]) * ih1
