Prove2Me

lean_workbook_plus_17898

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let α,β>0\alpha,\beta>0 and a sequence (an)n≥0(a_n)_{n\ge 0} for which α⋅an+1+β⋅an=0\alpha\cdot a_{n+1}+\beta \cdot a_n=0. Study the nature of this sequence.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_17898 (α β : ℝ) (a : ℕ → ℝ) (hα : α > 0) (hβ : β > 0) (ha : ∀ n, α * a (n + 1) + β * a n = 0) : ∃ k : ℝ, ∀ n, a (n + 1) = k * a n   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph