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 highlevel view. 
BibTeX: 
@article{Gaussian_IntegersAFP,
author = {Manuel Eberl},
title = {Gaussian Integers},
journal = {Archive of Formal Proofs},
month = apr,
year = 2020,
note = {\url{http://isaafp.org/entries/Gaussian_Integers.html},
Formal proof development},
ISSN = {2150914x},
}
