T_sub_two

Mathlib.RingTheory.Polynomial.Chebyshev

URI: https://scilib.ai/kg/mathlib#Polynomial.Chebyshev.T_sub_two

English

The Chebyshev polynomial satisfies T(n−1) = 2 X T(n) − T(n+1) for integers n.

Русский

Чебышёв полином удовлетворяет T(n−1) = 2 X T(n) − T(n+1) для целых n.

LaTeX

$$$T_R(n-1) = 2 \\cdot X \\cdot T_R(n) - T_R(n+1)$$$

Lean4

theorem T_sub_two (n : ℤ) : T R (n - 2) = 2 * X * T R (n - 1) - T R n := by
  linear_combination (norm := ring_nf) T_add_two R (n - 2)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru