mathlib

e25a3174 - feat(number_theory/diophantine_approximation): add Legendre's thm on rat'l approximations (#18460)

feat(number_theory/diophantine_approximation): add Legendre's thm on rat'l approximations (#18460) This adds *Legendre's Theorem* on rational approximations: ```lean lemma ex_continued_fraction_convergent_eq_rat {ξ : ℝ} {q : ℚ} (h : |ξ - q| < 1 / (2 * q.denom ^ 2)) : ∃ n, (generalized_continued_fraction.of ξ).convergents n = q ``` See this [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Diophantine.20approximation/near/323758115). Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>