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.
@[instance]
@[instance]
Equations
The embedding of the Gaussian integers into the complex numbers, as a ring homomorphism.
@[instance]
Equations
@[simp]
@[simp]
theorem
gaussian_int.nat_cast_complex_norm
(x : gaussian_int) :
↑(zsqrtd.norm x) = ↑(complex.norm_sq ↑x)
@[simp]
theorem
gaussian_int.coe_nat_abs_norm
(x : gaussian_int) :
↑((zsqrtd.norm x).nat_abs) = zsqrtd.norm x
@[simp]
theorem
gaussian_int.nat_cast_nat_abs_norm
{α : Type u_1}
[ring α]
(x : gaussian_int) :
↑((zsqrtd.norm x).nat_abs) = ↑(zsqrtd.norm x)
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)}
@[instance]
Equations
@[instance]
Equations
theorem
gaussian_int.norm_mod_lt
(x : gaussian_int)
{y : gaussian_int} :
y ≠ 0 → zsqrtd.norm (x % y) < zsqrtd.norm y
theorem
gaussian_int.nat_abs_norm_mod_lt
(x : gaussian_int)
{y : gaussian_int} :
y ≠ 0 → (zsqrtd.norm (x % y)).nat_abs < (zsqrtd.norm y).nat_abs
@[instance]
Equations
@[instance]
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 := _, neg := comm_ring.neg gaussian_int.comm_ring, 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 := _, 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}