fibRec_charPoly_eq — Mathlib

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]

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