C_sub_two

Mathlib.RingTheory.Polynomial.Chebyshev

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

English

For every integer n, C(n-2) = X C(n-1) − C(n).

Русский

Для каждого целого n верно C(n-2) = X C(n-1) − C(n).

LaTeX

$$$ C(n-2) = X C(n-1) - C(n) $$$

Lean4

theorem C_sub_two (n : ℤ) : C R (n - 2) = X * C R (n - 1) - C R n := by
  linear_combination (norm := ring_nf) C_add_two R (n - 2)

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

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

Разделы

Аффилиация

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