C_two_mul_complex_cosh — Mathlib

English

The n-th rescaled Chebyshev polynomial of the first kind satisfies C_n(2 cosh θ) = 2 cosh(n θ).

Русский

Умножение: C_n(2 cosh θ) = 2 cosh(n θ).

LaTeX

$$$(C \mathbb{C} n).eval (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_complex_cosh (n : ℤ) : (C ℂ n).eval (2 * cosh θ) = 2 * cosh (n * θ) := by
  simp [C_eq_two_mul_T_comp_half_mul_X]

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