C_two_mul_real_cos — Mathlib

English

Let θ be a real number and n an integer. The n-th rescaled Chebyshev polynomial of the first kind (Vieta–Lucas) evaluated at 2 cos θ equals 2 cos(n θ).

Русский

Пусть θ — вещественное число и n — целое число. n-й масштабированный полином Чебышёва первого рода (Вьета–Лукас) в точке 2 cos θ равен 2 cos(n θ).

LaTeX

$$$$C_n(2 \\cos \\theta) = 2 \\cos(n \\theta)$$$$

Lean4

/-- The `n`-th rescaled Chebyshev polynomial of the first kind (Vieta–Lucas polynomial) evaluates on
`2 * cos θ` to the value `2 * cos (n * θ)`. -/
@[simp]
theorem C_two_mul_real_cos : (C ℝ n).eval (2 * cos θ) = 2 * cos (n * θ) :=
  mod_cast C_two_mul_complex_cos θ n

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