C_eq_S_sub_X_mul_S

Mathlib.RingTheory.Polynomial.Chebyshev

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

English

For all integers n, C_R(n) = 2 S_R(n) - X S_R(n-1).

Русский

Для всех n: C_R(n) = 2 S_R(n) - X S_R(n-1).

LaTeX

$$$ C_R(n) = 2 \; S_R(n) - X \; S_R(n-1) $$$

Lean4

theorem C_eq_S_sub_X_mul_S (n : ℤ) : C R n = 2 * S R n - X * S R (n - 1) := by
  linear_combination (norm := ring_nf) -S_eq_X_mul_S_add_C R (n - 1)

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

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

Разделы

Аффилиация

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