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.

The homomorphism to_complex into the complex numbers is also defined in this file.

Main statements

prime_iff_mod_four_eq_three_of_nat_prime A prime natural number is prime in ℤ[i] if and only if it is 3 mod 4

Notations

This file uses the local notation ℤ[i] for gaussian_int

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.