GeneralizedContinuedFraction.convergents_succ

theorem GeneralizedContinuedFraction.convergents_succ : ∀ {K : Type u_1} (v : K) [inst : LinearOrderedField K] [inst_1 : FloorRing K] (n : ℕ), (GeneralizedContinuedFraction.of v).convergents (n + 1) = ↑⌊v⌋ + 1 / (GeneralizedContinuedFraction.of (Int.fract v)⁻¹).convergents n

This theorem describes the recurrence relation for the `convergents` of the generalized continued fraction expansion of an element `v` of a linear ordered field `K`. It states that the `n+1`-th `convergent` of `v` is equal to the floor of `v` plus the reciprocal of the `n`-th `convergent` of the inverse of the fractional part of `v`. Here, the floor of `v` is denoted by `⌊v⌋`, the `n`-th `convergent` is obtained using `GeneralizedContinuedFraction.of v.convergents n`, the fractional part of `v` is obtained by `Int.fract v`, and the inverse is denoted with `⁻¹`.

More concisely: The `(n+1)`-th convergent of the generalized continued fraction expansion of an element `v` in a linear ordered field `K` is given by `⌊v⌋ + (1 / (GeneralizedContinuedFraction.of v.convergents n)).⁻¹`, where `Int.fract v` represents the fractional part of `v`.