mathlib

552ebeb0 - feat(algebra/continued_fractions): add convergence theorem (#6607)

feat(algebra/continued_fractions): add convergence theorem (#6607) 1. Add convergence theorem for continued fractions, i.e. `(gcf.of v).convergents` converges to `v`. 2. Add some simple corollaries following from the already existing approximation lemmas for continued fractions, e.g. the equivalence of the convergent computations for continued fractions computed by `gcf.of` (`(gcf.of v).convergents` and `(gcf.of v).convergents'`).