# mathlib3documentation

algebra.continued_fractions.terminated_stable

# Stabilisation of gcf Computations Under Termination #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Summary #

We show that the continuants and convergents of a gcf stabilise once the gcf terminates.

theorem generalized_continued_fraction.terminated_stable {K : Type u_1} {n m : } (n_le_m : n m) (terminated_at_n : g.terminated_at n) :

If a gcf terminated at position n, it also terminated at m ≥ n.

theorem generalized_continued_fraction.continuants_aux_stable_of_terminated {K : Type u_1} {n m : } (n_lt_m : n < m) (terminated_at_n : g.terminated_at n) :
theorem generalized_continued_fraction.convergents'_aux_stable_of_terminated {K : Type u_1} {n m : } (n_le_m : n m) (terminated_at_n : s.terminated_at n) :
theorem generalized_continued_fraction.continuants_stable_of_terminated {K : Type u_1} {n m : } (n_le_m : n m) (terminated_at_n : g.terminated_at n) :
theorem generalized_continued_fraction.numerators_stable_of_terminated {K : Type u_1} {n m : } (n_le_m : n m) (terminated_at_n : g.terminated_at n) :
theorem generalized_continued_fraction.denominators_stable_of_terminated {K : Type u_1} {n m : } (n_le_m : n m) (terminated_at_n : g.terminated_at n) :
theorem generalized_continued_fraction.convergents_stable_of_terminated {K : Type u_1} {n m : } (n_le_m : n m) (terminated_at_n : g.terminated_at n) :
theorem generalized_continued_fraction.convergents'_stable_of_terminated {K : Type u_1} {n m : } (n_le_m : n m) (terminated_at_n : g.terminated_at n) :