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:
- The characterisation of all positive integers that can be written as sums of two squares
- 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.