### Abstract

The Gaussian integers are the subring ℤ[i] of the complex numbers, i. e. the ring of all complex numbers with integral real and imaginary part. This article provides a definition of this ring as well as proofs of various basic properties, such as that they form a Euclidean ring and a full classification of their primes. An executable (albeit not very efficient) factorisation algorithm is also provided.

Lastly, this Gaussian integer formalisation is used in two short applications:

1. The characterisation of all positive integers that can be written as sums of two squares
2. Euclid's formula for primitive Pythagorean triples

While elementary proofs for both of these are already available in the AFP, the theory of Gaussian integers provides more concise proofs and a more high-level view.

### License

BSD License

### Topics

- Mathematics/Number theory

### Session Gaussian_Integers

- Gaussian_Integers
- Gaussian_Integers_Test
- Gaussian_Integers_Sums_Of_Two_Squares
- Gaussian_Integers_Pythagorean_Triples
- Gaussian_Integers_Everything

### Depends on

- Polynomial Factorization

## Cite

×

Gaussian_Integers-AFP

    @article{Gaussian_Integers-AFP,
      author  = {Manuel Eberl},
      title   = {Gaussian Integers},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Gaussian_Integers.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 30, 2020 : Isabelle2020