# 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.

theorem GeneralizedContinuedFraction.part_num_eq_s_a {α : Type u_1} {g : } {n : } (s_nth_eq : Stream'.Seq.get? g.s n = some gp) :
theorem GeneralizedContinuedFraction.part_denom_eq_s_b {α : Type u_1} {g : } {n : } (s_nth_eq : Stream'.Seq.get? g.s n = some gp) :
theorem GeneralizedContinuedFraction.exists_s_a_of_part_num {α : Type u_1} {g : } {n : } {a : α} (nth_part_num_eq : ) :
gp, Stream'.Seq.get? g.s n = some gp gp.a = a
theorem GeneralizedContinuedFraction.exists_s_b_of_part_denom {α : Type u_1} {g : } {n : } {b : α} (nth_part_denom_eq : ) :
gp, Stream'.Seq.get? g.s 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 GeneralizedContinuedFraction.num_eq_conts_a {K : Type u_1} {g : } {n : } [] :
theorem GeneralizedContinuedFraction.exists_conts_a_of_num {K : Type u_1} {g : } {n : } [] {A : K} (nth_num_eq : ) :
conts, conts.a = A
theorem GeneralizedContinuedFraction.exists_conts_b_of_denom {K : Type u_1} {g : } {n : } [] {B : K} (nth_denom_eq : ) :
conts, conts.b = B
@[simp]
theorem GeneralizedContinuedFraction.zeroth_continuant_aux_eq_one_zero {K : Type u_1} {g : } [] :
= { a := 1, b := 0 }
@[simp]
theorem GeneralizedContinuedFraction.first_continuant_aux_eq_h_one {K : Type u_1} {g : } [] :
= { a := g.h, b := 1 }
@[simp]
theorem GeneralizedContinuedFraction.zeroth_continuant_eq_h_one {K : Type u_1} {g : } [] :
= { a := g.h, b := 1 }
theorem GeneralizedContinuedFraction.second_continuant_aux_eq {K : Type u_1} {g : } [] (zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp) :
= { a := gp.b * g.h + gp.a, b := gp.b }
theorem GeneralizedContinuedFraction.first_continuant_eq {K : Type u_1} {g : } [] (zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp) :
= { a := gp.b * g.h + gp.a, b := gp.b }
theorem GeneralizedContinuedFraction.first_numerator_eq {K : Type u_1} {g : } [] (zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp) :
= gp.b * g.h + gp.a
theorem GeneralizedContinuedFraction.first_denominator_eq {K : Type u_1} {g : } [] (zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp) :
@[simp]
theorem GeneralizedContinuedFraction.convergents'Aux_succ_some {K : Type u_1} [] (h : ) (n : ) :
= p.a / ()