S_two_mul_real_cos — Mathlib

English

Let θ be a real number and n an integer. The n-th rescaled Chebyshev polynomial of the second kind evaluated at 2 cos θ, multiplied by sin θ, equals sin((n+1) θ).

Русский

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

LaTeX

$$$$S_n(2 \\cos \\theta) \\sin \\theta = \\sin((n+1) \\theta)$$$$

Lean4

/-- The `n`-th rescaled Chebyshev polynomial of the second kind (Vieta–Fibonacci polynomial)
evaluates on `2 * cos θ` to the value `sin ((n + 1) * θ) / sin θ`. -/
@[simp]
theorem S_two_mul_real_cos : (S ℝ n).eval (2 * cos θ) * sin θ = sin ((n + 1) * θ) :=
  mod_cast S_two_mul_complex_cos θ n

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