Cassinis_Identity
Provedfibonacci-numbersproofwiki
F_{n+1} * F_{n-1} - F_n^2 = (-1)^n (Cassini's identity for Fibonacci numbers).
Preamble
import Mathlib.Data.Nat.Fib.Basic import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Cassinis_Identity (n : ℕ) (hn : 0 < n) : (Nat.fib (n + 1) : ℤ) * Nat.fib (n - 1) - (Nat.fib n : ℤ) ^ 2 = (-1) ^ n := by sorry
Source