Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-14 00:42 552ebeb0

View on Github →

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').

Estimated changes