# mathlibdocumentation

data.zsqrtd.gaussian_int

# 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.

def gaussian_int  :
Type

Equations
@[instance]

Equations
@[instance]

Equations

The embedding of the Gaussian integers into the complex numbers, as a ring homomorphism.

Equations
@[instance]

Equations
theorem gaussian_int.to_complex_def' (x y : ) :
{re := x, im := y} = x + (y) * complex.I

@[simp]

@[simp]

@[simp]
theorem gaussian_int.to_complex_re (x y : ) :
{re := x, im := y}.re = x

@[simp]
theorem gaussian_int.to_complex_im (x y : ) :
{re := x, im := y}.im = y

@[simp]
theorem gaussian_int.to_complex_add (x y : gaussian_int) :
(x + y) = x + y

@[simp]
theorem gaussian_int.to_complex_mul (x y : gaussian_int) :
x * y = (x) * y

@[simp]

@[simp]

@[simp]
theorem gaussian_int.to_complex_sub (x y : gaussian_int) :
(x - y) = x - y

@[simp]

@[simp]

@[simp]
theorem gaussian_int.norm_eq_zero {x : gaussian_int} :
= 0 x = 0

@[simp]

Equations
@[instance]

Equations
theorem gaussian_int.div_def (x y : gaussian_int) :
x / y = {re := round (((x * .re) / (zsqrtd.norm y)), im := round (((x * .im) / (zsqrtd.norm y))}

theorem gaussian_int.norm_sq_le_norm_sq_of_re_le_of_im_le {x y : } (hre : abs x.re abs y.re) (him : abs x.im abs y.im) :

Equations
@[instance]

Equations
theorem gaussian_int.mod_def (x y : gaussian_int) :
x % y = x - y * (x / y)

theorem gaussian_int.norm_mod_lt (x : gaussian_int) {y : gaussian_int} (hy : y 0) :
zsqrtd.norm (x % y) <

@[instance]

@[instance]

Equations
theorem gaussian_int.sum_two_squares_of_nat_prime_of_not_irreducible (p : ) [hp : fact (nat.prime p)] (hpi : ¬) :
∃ (a b : ), a ^ 2 + b ^ 2 = p

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