### Abstract

This article gives the basic theory of Pell's equation x2 = 1 + D y2, where D∈ ℕ is a parameter and x, y are integer variables.

The main result that is proven is the following: If D is not a perfect square, then there exists a fundamental solution (x0, y0) that is not the trivial solution (1, 0) and which generates all other solutions (x, y) in the sense that there exists some n∈ ℕ such that |x| + |y| √D = (x0 + y0√D)n. This also implies that the set of solutions is infinite, and it gives us an explicit and executable characterisation of all the solutions.

Based on this, simple executable algorithms for computing the fundamental solution and the infinite sequence of all non-negative solutions are also provided.

### License

BSD License

### Topics

- Mathematics/Number theory

### Session Pell

- Efficient_Discrete_Sqrt
- Pell
- Pell_Algorithm
- Pell_Algorithm_Test

### Used by

- Continued Fractions
- Mersenne primes and the Lucas–Lehmer test

## Cite

×

Pell-AFP

    @article{Pell-AFP,
      author  = {Manuel Eberl},
      title   = {Pell's Equation},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Pell.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Jun 25, 2018 : Isabelle2017