chebyshev_U_eq_dickson_two_one — Mathlib

English

The Chebyshev polynomial Chebyshev.U R n is the composition of the Dickson polynomial 2,1 n with a factor 2: Chebyshev.U R n = (dickson 2 1 n).comp (2 X).

Русский

Chebyshev U через Диксон: Chebyshev U_R(n) = (dickson 2 1 n).comp (2 X).

LaTeX

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

Lean4

theorem chebyshev_U_eq_dickson_two_one (n : ℕ) : Chebyshev.U R n = (dickson 2 (1 : R) n).comp (2 * X) :=
  dickson_two_one_eq_chebyshev_S R n ▸ (Chebyshev.S_comp_two_mul_X R n).symm

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