Commit 2023-02-25 19:13 c23aca35

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:

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.