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.

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.

def pell.solution₁ (d : ) :

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₁
@[protected, instance]
@[protected, instance]
@[protected]

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

Equations
@[protected]

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

Equations
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

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.

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.

@[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.

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

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

Equations
@[simp]
theorem pell.solution₁.x_mk {d : } (x y : ) (prop : x ^ 2 - d * y ^ 2 = 1) :
(pell.solution₁.mk x y prop).x = x
@[simp]
theorem pell.solution₁.y_mk {d : } (x y : ) (prop : x ^ 2 - d * y ^ 2 = 1) :
(pell.solution₁.mk x y prop).y = y
@[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}
@[simp]
theorem pell.solution₁.x_one {d : } :
1.x = 1
@[simp]
theorem pell.solution₁.y_one {d : } :
1.y = 0
@[simp]
theorem pell.solution₁.x_mul {d : } (a b : pell.solution₁ d) :
(a * b).x = a.x * b.x + d * (a.y * b.y)
@[simp]
theorem pell.solution₁.y_mul {d : } (a b : pell.solution₁ d) :
(a * b).y = a.x * b.y + a.y * b.x
@[simp]
theorem pell.solution₁.x_inv {d : } (a : pell.solution₁ d) :
a⁻¹.x = a.x
@[simp]
theorem pell.solution₁.y_inv {d : } (a : pell.solution₁ d) :
a⁻¹.y = -a.y
@[simp]
theorem pell.solution₁.x_neg {d : } (a : pell.solution₁ d) :
(-a).x = -a.x
@[simp]
theorem pell.solution₁.y_neg {d : } (a : pell.solution₁ d) :
(-a).y = -a.y

Existence of nontrivial solutions #

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.

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.

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.