Pell's Equation #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
number_theory.pell_matiyasevic, 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
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.
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,
pell.is_fundamental.eq_zpow_or_neg_zpow, and that a (positive) solution has this property
if and only if it is fundamental, see
- Extend to
x ^ 2 - d * y ^ 2 = -1and further generalizations.
- Connect solutions to the continued fraction expansion of
Group structure of the solution set #
We define a structure of a commutative multiplicative group with distributive negation
on the set of all solutions to the Pell equation
x^2 - d*y^2 = 1.
The type of such solutions is
pell.solution₁ d. It corresponds to a pair of integers
and a proof that
(x, y) is indeed a solution.
The multiplication is given by
(x, y) * (x', y') = (x*y' + d*y*y', x*y' + y*x').
This is obtained by mapping
(x, y) to
x + y*√d and multiplying the results.
In fact, we define
pell.solution₁ d to be
↥(unitary (ℤ√d)) and transport
the "commutative group with distributive negation" structure from
We then set up an API for
An element of
ℤ√d has norm one (i.e.,
a.re^2 - d*a.im^2 = 1) if and only if
it is contained in the submonoid of unitary elements.
TODO: merge this result with
pell.solution₁ d is the type of solutions to the Pell equation
x^2 - d*y^2 = 1.
We define this in terms of elements of
ℤ√d of norm one.
Existence of nontrivial solutions #
Fundamental solutions #
We define the notion of a fundamental solution of Pell's equation and
show that it exists and is unique (when
d is positive and non-square)
and generates the group of solutions up to sign.
d is positive and not a square, then the group of solutions to the Pell equation
x^2 - d*y^2 = 1 has a unique positive generator (up to sign).
A positive solution is a generator (up to sign) of the group of all solutions to the
x^2 - d*y^2 = 1 if and only if it is a fundamental solution.