mathlib3

c23aca35 - feat(number_theory/pell_general): add general existence result for Pell's Equation (#18484)

feat(number_theory/pell_general): add general existence result for Pell's Equation (#18484) This begins the development of the theory of Pell's Equation for general parameter `d` (a positive nonsquare integer). Note that the existing file `number_theory.pell` restricts to `d = a ^ 2 - 1` (which is sufficient for the application to prove Matiyasevich's theorem). This PR provides a proof of the existence of a nontrivial solution: ```lean theorem ex_nontriv_sol {d : ℤ} (h₀ : 0 < d) (hd : ¬ is_square d) : ∃ x y : ℤ, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0 ``` We follow the (standard) proof given in Ireland-Rosen, which uses Dirichlet's approximation theorem and multiple instances of the pigeonhole principle to obtain two distinct solutions of `x^2 - d*y^2 = m` (for some `m`) that are congruent mod `m`; a nontrivial solution of the original equation is then obtained by "dividing" one by the other. See [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Proving.20Pell's.20equation.20is.20solvable/near/322885832).