fast_fib_aux_bit_tt

Mathlib.Data.Nat.Fib.Basic

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

Lean4

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

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

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

Разделы

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

Аффилиация

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