Commit 2023-03-09 10:11 5b05c634

feat(number_theory/pell): add exists_pos_of_not_is_square (#18567) This PR continues work on the theory of the Pell equation for general (nonsquare and positive) d. In preparation for proving statements on the structure of the solution set, this adds

lemma exists_pos_of_not_is_square {d : ℤ} (h₀ : 0 < d) (hd : ¬ is_square d) :
  ∃ x y : ℤ, x ^ 2 - d * y ^ 2 = 1 ∧ 1 < x ∧ 0 < y := ...

as a prerequisite for defining the fundamental solution as the solution with smallest x > 1 and positive y. See this thread on Zulip.