α : Type ?u.57955
inst✝ : CommSemiring α
⊢ IsRoot (X ^ 2 - (X + 1)) φ
α : Type ?u.57955
inst✝ : CommSemiring α
⊢ LinearRecurrence.IsSolution fibRec fun x => φ ^ x
rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]
no goals
α : Type ?u.57955
inst✝ : CommSemiring α
⊢ IsRoot (X ^ 2 - (X + 1)) φ
simp [sub_eq_zero, - div_pow]