# Documentation

Mathlib.NumberTheory.Pell

# Pell's Equation #

Pell's Equation is the equation $x^2 - d y^2 = 1$, where $d$ is a positive integer that is not a square, and one is interested in solutions in integers $x$ and $y$.

In this file, we aim at providing all of the essential theory of Pell's Equation for general $d$ (as opposed to the contents of NumberTheory.PellMatiyasevic, which is specific to the case $d = a^2 - 1$ for some $a > 1$).

We begin by defining a type Pell.Solution₁ d for solutions of the equation, show that it has a natural structure as an abelian group, and prove some basic properties.

We then prove the following

Theorem. Let $d$ be a positive integer that is not a square. Then the equation $x^2 - d y^2 = 1$ has a nontrivial (i.e., with $y \ne 0$) solution in integers.

See Pell.exists_of_not_isSquare and Pell.Solution₁.exists_nontrivial_of_not_isSquare.

We then define the fundamental solution to be the solution with smallest $x$ among all solutions satisfying $x > 1$ and $y > 0$. We show that every solution is a power (in the sense of the group structure mentioned above) of the fundamental solution up to a (common) sign, see Pell.IsFundamental.eq_zpow_or_neg_zpow, and that a (positive) solution has this property if and only if it is fundamental, see Pell.pos_generator_iff_fundamental.

• [K. Ireland, M. Rosen, A classical introduction to modern number theory (Section 17.5)][IrelandRosen1990]

Pell's equation

## TODO #

• Extend to x ^ 2 - d * y ^ 2 = -1 and further generalizations.
• Connect solutions to the continued fraction expansion of √d.