mathlib3 documentation

algebra.continued_fractions.translations

Basic Translation Lemmas Between Functions Defined for Continued Fractions #

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

Summary #

Some simple translation lemmas between the different definitions of functions defined in algebra.continued_fractions.basic.

Translations Between General Access Functions #

Here we give some basic translations that hold by definition between the various methods that allow us to access the numerators and denominators of a continued fraction.

Translations Between Computational Functions #

Here we give some basic translations that hold by definition for the computational methods of a continued fraction.