Documentation

Mathlib.Algebra.ContinuedFractions.Translations

Basic Translation Lemmas Between Functions Defined for Continued Fractions #

Summary #

Some simple translation lemmas between the different definitions of functions defined in Algebra.ContinuedFractions.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.