lean_workbook_plus_61921
OpenProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61921 (n : ℕ) : ∑ k in Finset.range (n+1), fib k ^ 2 = fib n * fib (n + 1) := by sorry
Source
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_61921 (n : ℕ) : ∑ k in Finset.range (n+1), fib k ^ 2 = fib n * fib (n + 1) := by sorry