C_natAbs

Mathlib.RingTheory.Polynomial.Chebyshev

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

English

For any integer n, C_R(n.natAbs) = C_R(n).

Русский

Для целого n верно C_R(|n|) = C_R(n).

LaTeX

$$$ C_R(n\natexlab{.natAbs}) = C_R(n) $$$

Lean4

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

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

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

Разделы

Аффилиация

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