fast_fib_aux_bit_ff

Mathlib.Data.Nat.Fib.Basic

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

Lean4

theorem fast_fib_aux_bit_ff (n : ℕ) :
    fastFibAux (bit false n) =
      let p := fastFibAux n
      (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2) :=
  by
  rw [fastFibAux, binaryRec_eq]
  · rfl
  · simp

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

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

Разделы

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

Аффилиация

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