fib_two_mul

Mathlib.Data.Nat.Fib.Basic

URI: https://scilib.ai/kg/mathlib#Nat.fib_two_mul

← MathLib Explorer

English

For all n, fib(2n) = fib(n) (2 fib(n+1) − fib(n)).

Русский

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

LaTeX

$$fib(2n) = fib(n) (2 fib(n+1) - fib(n))$$

Lean4

theorem fib_two_mul (n : ℕ) : fib (2 * n) = fib n * (2 * fib (n + 1) - fib n) :=
  by
  cases n
  · simp
  · rw [two_mul, ← add_assoc, fib_add, fib_add_two, two_mul]
    simp only [← add_assoc, add_tsub_cancel_right]
    ring

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru