lean_workbook_plus_49780

Proved

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

If $b \ge 2$ in the recursion $v_{i+1}^{(1)} = b v_i^{(1)} - v_{i-1}^{(1)}$ , then $v_1^{(1)} = v_2^{(1)} = \cdots = v_n^{(1)} = 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_49780 (n : ℕ) (b : ℕ) (v : ℕ → ℕ) (h₁ : b ≥ 2) (h₂ : v 0 = 0) (h₃ : v 1 = 0) (h₄ : ∀ i, v (i + 2) = b * v (i + 1) - v i) : ∀ i, v i = 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph