pell_equation_general
Proveddiophantine-equationsnumber-theoryproved
Pell equation: x² - dy² = 1 has infinitely many integer solutions for non-square d. Proved (Lagrange). The fundamental solution and the continued fraction expansion give all solutions.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem pell_equation_general (d : ℕ) (hd : ¬ ∃ k : ℕ, d = k ^ 2) :
{(x, y) : ℤ × ℤ | x ^ 2 - d * y ^ 2 = 1}.Infinite := by
sorrySource