dickson_one_one_eq_chebyshev_T — Mathlib

English

If 2 is invertible in R, then the Dickson polynomial D_1,1(n) equals 2 times Chebyshev T applied to n after a suitable linear change: D_1,1(n) = 2 * Chebyshev.T_R(n) ∘ (C(1/2) * X).

Русский

Если 2 является обратимым в R, то D_1,1(n) равен 2 умноженному на Chebyshev T_R(n) после подходящего линейного отображения: D_1,1(n) = 2 * Chebyshev.T_R(n) ∘ (C(1/2) * X).

LaTeX

$$[Invertible (2 : R)] (dickson 1 (1 : R) n) = 2 * (Chebyshev.T R n).comp (C (⅟2) * X)$$

Lean4

theorem dickson_one_one_eq_chebyshev_T [Invertible (2 : R)] (n : ℕ) :
    dickson 1 (1 : R) n = 2 * (Chebyshev.T R n).comp (C (⅟2) * X) :=
  (dickson_one_one_eq_chebyshev_C R n).trans (Chebyshev.C_eq_two_mul_T_comp_half_mul_X R n)

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