fib_add — Mathlib

English

For all m,n, fib(m+n+1) = fib(m) fib(n) + fib(m+1) fib(n+1).

Русский

Для всех m,n выполняется fib(m+n+1) = fib(m) fib(n) + fib(m+1) fib(n+1).

LaTeX

$$fib(m+n+1) = fib(m) fib(n) + fib(m+1) fib(n+1)$$

Lean4

/-- See https://proofwiki.org/wiki/Fibonacci_Number_in_terms_of_Smaller_Fibonacci_Numbers -/
theorem fib_add (m n : ℕ) : fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1) := by
  induction n generalizing m with
  | zero => simp
  | succ n ih =>
    specialize ih (m + 1)
    rw [add_assoc m 1 n, add_comm 1 n] at ih
    simp only [fib_add_two, ih]
    ring

Похожие утверждения