dickson_one_one_eq_chebyshev_C — Mathlib

English

For all n, the Dickson polynomial with k = 1 and a = 1 equals Chebyshev C evaluated at n: D_1,1(n) = Chebyshev.C_R(n).

Русский

Для всех n полином Диксона при k = 1 и a = 1 равен Chebyshev C(n).

LaTeX

$$dickson\, 1\, (1)\, n = Chebyshev.C\, R\, n$$

Lean4

theorem dickson_one_one_eq_chebyshev_C : ∀ n, dickson 1 (1 : R) n = Chebyshev.C R n
  | 0 => by
    simp only [dickson_zero]
    norm_num
  | 1 => by rw [dickson_one, Nat.cast_one, Chebyshev.C_one]
  | n + 2 =>
    by
    rw [dickson_add_two, C_1, Nat.cast_add, Nat.cast_two, Chebyshev.C_add_two, dickson_one_one_eq_chebyshev_C (n + 1),
      dickson_one_one_eq_chebyshev_C n]
    push_cast
    ring

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