Gaussian integers #
The Gaussian integers are complex integer, complex numbers whose real and imaginary parts are both integers.
Main definitions #
The Euclidean domain structure on
ℤ[i] is defined in this file.
GaussianInt.toComplex into the complex numbers is also defined in this file.
See also #
prime_iff_mod_four_eq_three_of_nat_prime: A prime natural number is prime in
ℤ[i]if and only if it is
This file uses the local notation
Implementation notes #
Gaussian integers are implemented using the more general definition
Zsqrtd, the type of integers
adjoined a square root of
d, in this case
-1. The definition is reducible, so that properties
and definitions about
Zsqrtd can easily be used.