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.
Equations
The embedding of the Gaussian integers into the complex numbers, as a ring homomorphism.
Equations
- gaussian_int.to_complex = ⇑zsqrtd.lift ⟨complex.I, gaussian_int.to_complex._proof_1⟩
Equations
Equations
- x.div y = let n : ℚ := (rat.of_int (zsqrtd.norm y))⁻¹, c : ℤ√-1 := zsqrtd.conj y in {re := round ((rat.of_int (x * c).re) * n), im := round ((rat.of_int (x * c).im) * n)}
Equations
Equations
Equations
- gaussian_int.euclidean_domain = {add := comm_ring.add gaussian_int.comm_ring, add_assoc := _, zero := comm_ring.zero gaussian_int.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul gaussian_int.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg gaussian_int.comm_ring, sub := comm_ring.sub gaussian_int.comm_ring, sub_eq_add_neg := _, gsmul := comm_ring.gsmul gaussian_int.comm_ring, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul gaussian_int.comm_ring, mul_assoc := _, one := comm_ring.one gaussian_int.comm_ring, one_mul := _, mul_one := _, npow := comm_ring.npow gaussian_int.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, quotient := has_div.div gaussian_int.has_div, quotient_zero := gaussian_int.euclidean_domain._proof_1, remainder := has_mod.mod gaussian_int.has_mod, quotient_mul_add_remainder_eq := gaussian_int.euclidean_domain._proof_2, r := measure (int.nat_abs ∘ zsqrtd.norm), r_well_founded := gaussian_int.euclidean_domain._proof_3, remainder_lt := gaussian_int.nat_abs_norm_mod_lt, mul_left_not_lt := gaussian_int.euclidean_domain._proof_4}