lean_workbook_plus_56030
Proved
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_56030 (n : ℕ) : ∃ (f : ℕ → ℕ), f 0 = 2 ∧ ∀ k, f (k + 1) = f 1 * f k - f (k - 1) := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_56030 (n : ℕ) : ∃ (f : ℕ → ℕ), f 0 = 2 ∧ ∀ k, f (k + 1) = f 1 * f k - f (k - 1) := by sorry