Theorems · Theorem · number theory

GenContFract.convs_succ

∀ {K : Type u_1} (v : K) [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : FloorRing K]
  (n : ℕ), (GenContFract.of v).convs (n + 1) = ↑⌊v⌋ + 1 / (GenContFract.of (Int.fract v)⁻¹).convs n

The recurrence relation for the convergents of the continued fraction expansion of an element v of K in terms of the convergents of the inverse of its fractional part.

Defined in

Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingFloorRing