Theorems · Theorem · number theory

GenContFract.succ_nth_fib_le_of_nth_den

∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K],
  n = 0 ∨ ¬(GenContFract.of v).TerminatedAt (n - 1) → ↑(Nat.fib (n + 1)) ≤ (GenContFract.of v).dens n

Shows that the nth denominator is greater than or equal to the n + 1th fibonacci number, that is Nat.fib (n + 1) ≤ Bₙ.

Defined in

Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Cited by

1 results in Mathlib

Foundations

Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderIsStrictOrderedRingFloorRing