# Documentation

Mathlib.NumberTheory.Zsqrtd.GaussianInt

# 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 GaussianInt.toComplex into the complex numbers is also defined in this file.

See NumberTheory.Zsqrtd.QuadraticReciprocity for:

• 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 GaussianInt

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

@[reducible]

The Gaussian integers, defined as ℤ√(-1).

Instances For

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

Instances For
theorem GaussianInt.toComplex_def (x : GaussianInt) :
= x.re + x.im * Complex.I
theorem GaussianInt.toComplex_def' (x : ) (y : ) :
GaussianInt.toComplex { re := x, im := y } = x +
theorem GaussianInt.toComplex_def₂ (x : GaussianInt) :
= { re := x.re, im := x.im }
@[simp]
theorem GaussianInt.to_real_re (x : GaussianInt) :
x.re = ().re
@[simp]
theorem GaussianInt.to_real_im (x : GaussianInt) :
x.im = ().im
@[simp]
theorem GaussianInt.toComplex_re (x : ) (y : ) :
(GaussianInt.toComplex { re := x, im := y }).re = x
@[simp]
theorem GaussianInt.toComplex_im (x : ) (y : ) :
(GaussianInt.toComplex { re := x, im := y }).im = y
@[simp]
theorem GaussianInt.toComplex_star (x : GaussianInt) :
= ↑(starRingEnd ((fun x => ) x)) ()
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem GaussianInt.nat_cast_natAbs_norm {α : Type u_1} [Ring α] (x : GaussianInt) :
↑() = ↑()
theorem GaussianInt.div_def (x : GaussianInt) (y : GaussianInt) :
x / y = { re := round ((x * star y).re / ↑()), im := round ((x * star y).im / ↑()) }
theorem GaussianInt.normSq_le_normSq_of_re_le_of_im_le {x : } {y : } (hre : |x.re| |y.re|) (him : |x.im| |y.im|) :
theorem GaussianInt.mod_def (x : GaussianInt) (y : GaussianInt) :
x % y = x - y * (x / y)
theorem GaussianInt.norm_mod_lt (x : GaussianInt) {y : GaussianInt} (hy : y 0) :
Zsqrtd.norm (x % y) <
theorem GaussianInt.sq_add_sq_of_nat_prime_of_not_irreducible (p : ) [hp : Fact ()] (hpi : ¬) :
a b, a ^ 2 + b ^ 2 = p