dickson_two_one_eq_chebyshev_U — Mathlib

English

The Dickson polynomial D_2,1(n) equals Chebyshev U evaluated at n with a half-scaling: D_2,1(n) = Chebyshev.U_R(n).comp (C(1/2) * X).

Русский

Полином Диксона D_2,1(n) равен Chebyshev U при n с половинным масштабированием: D_2,1(n) = Chebyshev.U_R(n).comp (C(1/2) * X).

LaTeX

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

Lean4

theorem dickson_two_one_eq_chebyshev_U [Invertible (2 : R)] (n : ℕ) :
    dickson 2 (1 : R) n = (Chebyshev.U R n).comp (C (⅟2) * X) :=
  (dickson_two_one_eq_chebyshev_S R n).trans (Chebyshev.S_eq_U_comp_half_mul_X R n)

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