# mathlibdocumentation

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.

theorem generalized_continued_fraction.part_num_eq_s_a {α : Type u_1} {n : }  :
g.s.nth n = some gp = some gp.a

theorem generalized_continued_fraction.part_denom_eq_s_b {α : Type u_1} {n : }  :
g.s.nth n = some gp = some gp.b

theorem generalized_continued_fraction.exists_s_a_of_part_num {α : Type u_1} {n : } {a : α} :
= some a(∃ (gp : , g.s.nth n = some gp gp.a = a)

theorem generalized_continued_fraction.exists_s_b_of_part_denom {α : Type u_1} {n : } {b : α} :
= some b(∃ (gp : , g.s.nth n = some gp gp.b = b)

### 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} {n : } {A : K} :
g.numerators n = A(∃ (conts : , g.continuants n = conts conts.a = A)

theorem generalized_continued_fraction.exists_conts_b_of_denom {K : Type u_1} {n : } {B : K} :
g.denominators n = B(∃ (conts : , g.continuants n = conts conts.b = B)

@[simp]

@[simp]
theorem generalized_continued_fraction.first_continuant_aux_eq_h_one {K : Type u_1}  :
= {a := g.h, b := 1}

@[simp]
theorem generalized_continued_fraction.zeroth_continuant_eq_h_one {K : Type u_1}  :
g.continuants 0 = {a := g.h, b := 1}

@[simp]

theorem generalized_continued_fraction.second_continuant_aux_eq {K : Type u_1}  :
g.s.nth 0 = some gp = {a := (gp.b) * g.h + gp.a, b := gp.b}

theorem generalized_continued_fraction.first_continuant_eq {K : Type u_1}  :
g.s.nth 0 = some gpg.continuants 1 = {a := (gp.b) * g.h + gp.a, b := gp.b}

theorem generalized_continued_fraction.first_numerator_eq {K : Type u_1}  :
g.s.nth 0 = some gpg.numerators 1 = (gp.b) * g.h + gp.a

theorem generalized_continued_fraction.first_denominator_eq {K : Type u_1}  :
g.s.nth 0 = some gpg.denominators 1 = gp.b