English
For any commutative ring β, fibRec has the same characteristic polynomial X^2 - (X + 1).
Русский
Для любого кольца β последовательность fibRec имеет характеристический многочлен X^2 - (X + 1).
LaTeX
$$$\forall \beta\ [\mathrm{CommRing}\ \beta],\ \ fibRec.charPoly = X^2 - (X + 1)$$$
Lean4
/-- As expected, the Fibonacci sequence is a solution of `fibRec`. -/
theorem fib_isSol_fibRec : fibRec.IsSolution (fun x => x.fib : ℕ → α) :=
by
rw [fibRec]
intro n
simp only
rw [Nat.fib_add_two, add_comm]
simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ']