mathlib3

9956c380 - feat(number_theory/diophantine_approximation): add more results (#18193)

feat(number_theory/diophantine_approximation): add more results (#18193) This PR adds the following results: ```lean lemma rat.finite_rat_abs_sub_lt_one_div_denom_sq (ξ : ℚ) : {q : ℚ | |ξ - q| < 1 / q.denom ^ 2}.finite lemma real.infinite_rat_abs_sub_lt_one_div_denom_sq_iff_irrational (ξ : ℝ) : {q : ℚ | |ξ - q| < 1 / q.denom ^ 2}.infinite ↔ irrational ξ ``` See the [discussion on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Diophantine.20approximation/near/321399454).