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