English
The characteristic polynomial of fibRec is X^2 - (X + 1).
Русский
Характеристический многочлен fibRec равен X^2 - (X + 1).
LaTeX
$$$\operatorname{charPoly}(\mathrm{fibRec}) = X^2 - (X + 1)$$$
Lean4
/-- The characteristic polynomial of `fibRec` is `X² - (X + 1)`. -/
theorem fibRec_charPoly_eq {β : Type*} [CommRing β] : fibRec.charPoly = X ^ 2 - (X + (1 : β[X])) :=
by
rw [fibRec, LinearRecurrence.charPoly]
simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ', ← smul_X_eq_monomial]