mathlib3 documentation


Corollaries From Approximation Lemmas (algebra.continued_fractions.computation.approximations) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Summary #

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 (generalized_continued_fraction.convergents and generalized_continued_fraction.convergents') for 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 #

Tags #

convergence, fractions

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 v of K in terms of the convergents of the inverse of its fractional part.

Convergence #

We next show that (generalized_continued_fraction.of v).convergents v converges to v.