T_eq_X_mul_T_sub_pol_U — Mathlib

English

For any integer n, (1 − X^2) U_n = X T_{n+1} − T_{n+2}.

Русский

Для любого целого n выполняется (1 − X^2) U_n = X T_{n+1} − T_{n+2}.

LaTeX

$$$ (1 - X^2) U(n) = X\,T(n+1) - T(n+2) $$$

Lean4

theorem T_eq_X_mul_T_sub_pol_U (n : ℤ) : T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n :=
  by
  have h₁ := U_eq_X_mul_U_add_T R n
  have h₂ := U_eq_X_mul_U_add_T R (n + 1)
  have h₃ := U_add_two R n
  linear_combination (norm := ring_nf) h₃ - h₂ + (X : R[X]) * h₁

Похожие утверждения