U_neg

Mathlib.RingTheory.Polynomial.Chebyshev

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

English

For all integers n, U(-n) = −U(n−2).

Русский

Для каждого целого n выполняется U(−n) = −U(n−2).

LaTeX

$$$ U(-n) = -U(n-2) $$$

Lean4

theorem U_neg (n : ℤ) : U R (-n) = -U R (n - 2) := by simpa [sub_sub] using U_neg_sub_one R (n - 1)

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

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

Разделы

Аффилиация

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