Gaussian Integers

Manuel Eberl 🌐

April 24, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Gaussian_Integers