Corollaries From Approximation Lemmas (
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.