Corollaries From Approximation Lemmas (
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
We show that the generalized_continued_fraction given by
generalized_continued_fraction.of in fact
is a (regular) continued fraction. Using the equivalence of the convergents computations
continued fractions (see
algebra.continued_fractions.convergents_equiv), it follows that the
convergents computations for
generalized_continued_fraction.of are equivalent.
Moreover, we show the convergence of the continued fractions computations, that is
(generalized_continued_fraction.of v).convergents indeed computes
v in the limit.
Main Definitions #
Main Theorems #
Creates the simple continued fraction of a value.
Creates the continued fraction of a value.
The recurrence relation for the
convergents of the continued fraction expansion
of an element
K in terms of the convergents of the inverse of its fractional part.