GeneralizedContinuedFraction.nth_cont_eq_succ_nth_cont_aux
theorem GeneralizedContinuedFraction.nth_cont_eq_succ_nth_cont_aux :
∀ {K : Type u_1} {g : GeneralizedContinuedFraction K} {n : ℕ} [inst : DivisionRing K],
g.continuants n = g.continuantsAux (n + 1)
This theorem states that for any type `K` equipped with a division ring structure, any generalized continued fraction `g` of type `K`, and any natural number `n`, the `n`-th continuant of `g` is equal to the (`n + 1`)-th auxiliary continuant of `g`. In simpler terms, it provides a relationship between the continuants and auxiliary continuants of a generalized continued fraction in a given division ring.
More concisely: For any division ring `K`, any generalized continued fraction `g` over `K`, and any natural number `n`, the `n`-th continuant and the `(n+1)`-th auxiliary continuant of `g` are equal.
|
GeneralizedContinuedFraction.terminatedAt_iff_s_none
theorem GeneralizedContinuedFraction.terminatedAt_iff_s_none :
∀ {α : Type u_1} {g : GeneralizedContinuedFraction α} {n : ℕ}, g.TerminatedAt n ↔ g.s.get? n = none
The theorem `GeneralizedContinuedFraction.terminatedAt_iff_s_none` states that for any type `α`, any generalized continued fraction `g` of type `α`, and any natural number `n`, the generalized continued fraction `g` is said to be terminated at position `n` if and only if the `n`th element of the sequence of `g` does not exist, i.e., is `none`. In other words, it provides a criterion for termination of a generalized continued fraction in terms of the absence of the `n`th element in its underlying sequence.
More concisely: A generalized continued fraction of type `α` is terminated at position `n` if and only if its `n`th element is `none`.
|
GeneralizedContinuedFraction.denom_eq_conts_b
theorem GeneralizedContinuedFraction.denom_eq_conts_b :
∀ {K : Type u_1} {g : GeneralizedContinuedFraction K} {n : ℕ} [inst : DivisionRing K],
g.denominators n = (g.continuants n).b
This theorem states that for any type `K` which forms a division ring, any generalized continued fraction `g` of type `K`, and any natural number `n`, the `n`th element of the denominators of `g` is equal to the second element (denoted by `.b`) of the `n`th pair of the continuants of `g`. In simpler terms, within the context of continued fractions, this theorem says that the `n`th denominator of a generalized continued fraction is equal to the `n`th second element of the continuants of the same fraction.
More concisely: For any division ring `K` and generalized continued fraction `g` of type `K`, the `n`th denominator is equal to the second element of the `n`th pair of continuants of `g`.
|