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. |
BibTeX: |
@article{Gaussian_Integers-AFP,
author = {Manuel Eberl},
title = {Gaussian Integers},
journal = {Archive of Formal Proofs},
month = apr,
year = 2020,
note = {\url{https://isa-afp.org/entries/Gaussian_Integers.html},
Formal proof development},
ISSN = {2150-914x},
}
|