S_two_mul_complex_cosh — Mathlib

English

The n-th rescaled Chebyshev polynomial of the second kind satisfies S_n(2 cosh θ) sinh θ = sinh((n+1) θ).

Русский

Умножение: S_n(2 cosh θ) sinh θ = sinh((n+1) θ).

LaTeX

$$(S \mathbb{C} n).eval (2 \cosh θ) \cdot \sinh θ = \sinh ((n + 1) θ)$$

Lean4

/-- The `n`-th rescaled Chebyshev polynomial of the second kind (Vieta–Fibonacci polynomial)
evaluates on `2 * cosh θ` to the value `sinh ((n + 1) * θ) / sinh θ`. -/
@[simp]
theorem S_two_mul_complex_cosh (n : ℤ) : (S ℂ n).eval (2 * cosh θ) * sinh θ = sinh ((n + 1) * θ) := by
  simp [S_eq_U_comp_half_mul_X]

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