mathlib documentation

number_theory.pell

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 #

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.

source
theorem pell.is_pell_solution_iff_mem_unitary {d : ℤ} {a : ℤ√d} :
a.re ^ 2 - d * a.im ^ 2 = 1 ↔ a ∈ unitary (ℤ√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.

source
def pell.solution₁ (d : ℤ) :
Type

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
Instances for pell.solution₁
source
@[protected, instance]
def pell.solution₁.comm_group (d : ℤ) :
comm_group (pell.solution₁ d)
source
@[protected, instance]
def pell.solution₁.has_distrib_neg (d : ℤ) :
has_distrib_neg (pell.solution₁ d)
source
@[protected, instance]
def pell.solution₁.inhabited (d : ℤ) :
inhabited (pell.solution₁ d)
source
@[protected, instance]
def pell.solution₁.zsqrtd.has_coe {d : ℤ} :
has_coe (pell.solution₁ d) (ℤ√d)
Equations
source
@[protected]
def pell.solution₁.x {d : ℤ} (a : pell.solution₁ d) :
ℤ

The x component of a solution to the Pell equation x^2 - d*y^2 = 1

Equations
source
@[protected]
def pell.solution₁.y {d : ℤ} (a : pell.solution₁ d) :
ℤ

The y component of a solution to the Pell equation x^2 - d*y^2 = 1

Equations
source
theorem pell.solution₁.prop {d : ℤ} (a : pell.solution₁ d) :
a.x ^ 2 - d * a.y ^ 2 = 1

The proof that a is a solution to the Pell equation x^2 - d*y^2 = 1

source
theorem pell.solution₁.prop_x {d : ℤ} (a : pell.solution₁ d) :
a.x ^ 2 = 1 + d * a.y ^ 2

An alternative form of the equation, suitable for rewriting x^2.

source
theorem pell.solution₁.prop_y {d : ℤ} (a : pell.solution₁ d) :
d * a.y ^ 2 = a.x ^ 2 - 1

An alternative form of the equation, suitable for rewriting d * y^2.

source
@[ext]
theorem pell.solution₁.ext {d : ℤ} {a b : pell.solution₁ d} (hx : a.x = b.x) (hy : a.y = b.y) :
a = b

Two solutions are equal if their x and y components are equal.

source
def pell.solution₁.mk {d : ℤ} (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1) :
pell.solution₁ d

Construct a solution from x, y and a proof that the equation is satisfied.

Equations
source
@[simp]
theorem pell.solution₁.x_mk {d : ℤ} (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1) :
(pell.solution₁.mk x y prop).x = x
source
@[simp]
theorem pell.solution₁.y_mk {d : ℤ} (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1) :
(pell.solution₁.mk x y prop).y = y
source
@[simp]
theorem pell.solution₁.coe_mk {d : ℤ} (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1) :
↑(pell.solution₁.mk x y prop) = {re := x, im := y}
source
@[simp]
theorem pell.solution₁.x_one {d : ℤ} :
1.x = 1
source
@[simp]
theorem pell.solution₁.y_one {d : ℤ} :
1.y = 0
source
@[simp]
theorem pell.solution₁.x_mul {d : ℤ} (a b : pell.solution₁ d) :
(a * b).x = a.x * b.x + d * (a.y * b.y)
source
@[simp]
theorem pell.solution₁.y_mul {d : ℤ} (a b : pell.solution₁ d) :
(a * b).y = a.x * b.y + a.y * b.x
source
@[simp]
theorem pell.solution₁.x_inv {d : ℤ} (a : pell.solution₁ d) :
a⁻¹.x = a.x
source
@[simp]
theorem pell.solution₁.y_inv {d : ℤ} (a : pell.solution₁ d) :
a⁻¹.y = -a.y
source
@[simp]
theorem pell.solution₁.x_neg {d : ℤ} (a : pell.solution₁ d) :
(-a).x = -a.x
source
@[simp]
theorem pell.solution₁.y_neg {d : ℤ} (a : pell.solution₁ d) :
(-a).y = -a.y

Existence of nontrivial solutions #

source
theorem pell.exists_of_not_is_square {d : ℤ} (h₀ : 0 < d) (hd : ¬is_square d) :
∃ (x y : ℤ), x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

If d is a positive integer that is not a square, then there is a nontrivial solution to the Pell equation x^2 - d*y^2 = 1.

source
theorem pell.exists_iff_not_is_square {d : ℤ} (h₀ : 0 < d) :
(∃ (x y : ℤ), x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0) ↔ ¬is_square d

If d is a positive integer, then there is a nontrivial solution to the Pell equation x^2 - d*y^2 = 1 if and only if d is not a square.

source
theorem pell.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

If d is a positive integer that is not a square, then there exists a solution to the Pell equation x^2 - d*y^2 = 1 with x > 1 and y > 0.