mathlib documentation

algebra.continued_fractions.translations

Basic Translation Lemmas Between Functions Defined for Continued Fractions

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.

theorem generalized_continued_fraction.exists_conts_a_of_num {K : Type u_1} {g : generalized_continued_fraction K} {n : } [division_ring K] {A : K} :
g.numerators n = A(∃ (conts : generalized_continued_fraction.pair K), g.continuants n = conts conts.a = A)