C — Mathlib · SciLib

English

The value at −2 is U_R(−2) = −1.

Русский

Значение при −2: U_R(−2) = −1.

LaTeX

$$$ U(-2) = -1 $$$

Lean4

/-- `C n` is the `n`th rescaled Chebyshev polynomial of the first kind (also known as a Vieta–Lucas
polynomial), given by $C_n(2x) = 2T_n(x)$. See `Polynomial.Chebyshev.C_comp_two_mul_X`. -/
noncomputable def C : ℤ → R[X]
  | 0 => 2
  | 1 => X
  | (n : ℕ) + 2 => X * C (n + 1) - C n
  | -((n : ℕ) + 1) => X * C (-n) - C (-n + 1)
termination_by n => Int.natAbs n + Int.natAbs (n - 1)

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