T_natAbs

Mathlib.RingTheory.Polynomial.Chebyshev

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

English

Chebyshev polynomials depend only on the nonnegative index: T_R(natAbs(n)) = T_R(n).

Русский

Чебышёвские полиномы зависят от неотрицательного индекса: T(n natAbs) = T(n).

LaTeX

$$T_R(n.natAbs) = T_R(n)$$

Lean4

theorem T_natAbs (n : ℤ) : T R n.natAbs = T R n := by obtain h | h := Int.natAbs_eq n <;> nth_rw 2 [h]; simp

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

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

Разделы

Аффилиация

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