T_real_cosh — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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