mathlib3

10d88727 - feat(algebra/continued_fractions/*): add some API lemmas (#18434)

feat(algebra/continued_fractions/*): add some API lemmas (#18434) This PR adds some API lemmas to the continued fractions files, leading to the recurrence ```lean lemma convergents_succ (v : K) (n : ℕ) : (of v).convergents (n + 1) = ⌊v⌋ + 1 / (of (int.fract v)⁻¹).convergents n ``` for the convergents of the continued fraction expansion of an element v of a linearly ordered floor field K. (Here `of` is `generalized_continued_fraction.of`.) This recurrence will then be used (in a later PR) for a proof of a theorem due to Legendre, which says that when x is a real number and p/q is a fraction such that |x - p/q| < 1/(2*q^2), then p/q is a convergent of the continued fraction expansion of x. See [this thread on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Diophantine.20approximation/near/327440641).