T_real_cos — Mathlib

English

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

Русский

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

LaTeX

$$$$T_n(\\cos \\theta) = \\cos(n \\theta)$$$$

Lean4

/-- The `n`-th Chebyshev polynomial of the first kind evaluates on `cos θ` to the
value `cos (n * θ)`. -/
@[simp]
theorem T_real_cos : (T ℝ n).eval (cos θ) = cos (n * θ) :=
  mod_cast T_complex_cos θ n

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