Theorems · Definition · number theory
Nat.fib
ℕ → ℕ
Implementation of the Fibonacci sequence satisfying
fib 0 = 0, fib 1 = 1, fib (n + 2) = fib n + fib (n + 1).
Note: We use a stream iterator for better performance when compared to the naive recursive
implementation.
- Defined in
- Mathlib.Data.Nat.Fib.Basic
- Cited by
- 74 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.iterateproof · cited by 740
Cited by79
Results whose statement or proof uses this declaration.
- Int.fibproof · cited by 26
- Nat.greatestFibproof · cited by 16
- Nat.fib_add_twostatement · cited by 13
- Nat.zeckendorfproof · cited by 7
- Nat.fastFibAuxproof · cited by 6
- Nat.fib_posstatement · cited by 4
- GenContFract.fib_le_of_contsAux_bstatement and proof · cited by 4
- Int.fib_negproof · cited by 4
- Int.fib_neg_natCaststatement and proof · cited by 4
- Nat.fib_le_fib_succstatement and proof · cited by 3
- Real.coe_fib_eqstatement · cited by 3
- Nat.zeckendorf_succstatement · cited by 3