Email Gateway (Aug 23 2022 at 08:51): Email Gateway (Aug 23 2022 at 08:51):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’m happy to announce a new AFP entry by Manuel Eberl:
Gaussian Integers
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.
Enjoy,
René
Last updated: Apr 26 2024 at 20:16 UTC