dickson_of_two_le — Mathlib

English

If n ≥ 2, then D_n = X D_{n-1} − C_a D_{n-2}. This follows from the n+2 recurrence by stepping down.

Русский

При n ≥ 2 справедливо D_n = X D_{n-1} − C_a D_{n-2}. Это следует из основной рекуррентности.

LaTeX

$$$dickson\, k\, a\, n = X \cdot dickson\, k\, a\, (n-1) - C\, a \cdot dickson\, k\, a\, (n-2)\quad\text{при } 2 \le n$$$

Lean4

theorem dickson_of_two_le {n : ℕ} (h : 2 ≤ n) : dickson k a n = X * dickson k a (n - 1) - C a * dickson k a (n - 2) :=
  by
  obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h
  rw [add_comm]
  exact dickson_add_two k a n

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