chebyshev_T_eq_dickson_one_one — Mathlib

English

The Chebyshev polynomial of the first kind is expressible through the Dickson polynomial of kind one by a simple rescaling and composition: Chebyshev.T_R(n) = (1/2) * (dickson 1 1 n).comp (2 * X).

Русский

Чебышёв полином первого рода выражим через полином Диксона первого рода: Chebyshev.T_R(n) = (1/2) * (dickson 1 1 n).comp (2 * X).

LaTeX

$$Chebyshev.T\, R\, n = C (⅟2) * (dickson 1 1 n).comp (2 * X)$$

Lean4

theorem chebyshev_T_eq_dickson_one_one [Invertible (2 : R)] (n : ℕ) :
    Chebyshev.T R n = C (⅟2) * (dickson 1 1 n).comp (2 * X) :=
  dickson_one_one_eq_chebyshev_C R n ▸ Chebyshev.T_eq_half_mul_C_comp_two_mul_X R n

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