fastFib

Mathlib.Data.Nat.Fib.Basic

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

← MathLib Explorer

English

The function fastFib is the first component of fastFibAux; hence fastFib(n) = fib(n).

Русский

Функция fastFib является первой компонентой fastFibAux; следовательно, fastFib(n) = fib(n).

LaTeX

$$fastFib(n) = fib(n)$$

Lean4

/-- Computes `Nat.fib n` using the binary representation of `n`.
Proved to be equal to `Nat.fib` in `Nat.fast_fib_eq`. -/
def fastFib (n : ℕ) : ℕ :=
  (fastFibAux n).1

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

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

Разделы

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

Аффилиация

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