C_two_mul_real_cosh — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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