dickson_two_one_eq_chebyshev_S — Mathlib

English

The Dickson polynomial D_2,1(n) of the second kind equals Chebyshev S evaluated at n: D_2,1(n) = Chebyshev.S_R(n).

Русский

Полином Диксона D_2,1(n) второго рода равен Chebyshev S при n: D_2,1(n) = Chebyshev.S_R(n).

LaTeX

$$dickson\, 2\, (1 : R)\, n = Chebyshev.S\, R\, n$$

Lean4

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

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