T_neg_one

Mathlib.RingTheory.Polynomial.Chebyshev

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

English

The Chebyshev polynomial at −1 equals X: T_R(−1) = X.

Русский

Чебышёв полином в −1 равен X: T_R(−1) = X.

LaTeX

$$$T_R(-1) = X$$$

Lean4

theorem T_neg_one : T R (-1) = X := by
  change T R (Int.negSucc 0) = X
  rw [T]
  suffices 2 * X - X = X by simpa
  ring

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

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

Разделы

Аффилиация

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