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