Pell's Equation #
We 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_is_square
.
This is the beginning of a development that aims 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$).
References #
Tags #
Pell's equation
TODO #
- Provide the structure theory of the solution set to Pell's equation
and furthermore also for
x ^ 2 - d * y ^ 2 = -1
and further generalizations. - Connect solutions to the continued fraction expansion of
√d
.
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 x
and y
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 ↥(unitary (ℤ√d))
.
We then set up an API for pell.solution₁ d
.
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.is_pell_iff_mem_unitary
.
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.
Equations
- pell.solution₁ d = ↥(unitary (ℤ√d))
Instances for pell.solution₁
Equations
- pell.solution₁.zsqrtd.has_coe = {coe := subtype.val (λ (x : ℤ√d), x ∈ unitary (ℤ√d))}
The x
component of a solution to the Pell equation x^2 - d*y^2 = 1
The y
component of a solution to the Pell equation x^2 - d*y^2 = 1