# 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, inline]

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

Equations
Instances For
Equations
Equations

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

Equations
Instances For
theorem GaussianInt.toComplex_def (x : GaussianInt) :
GaussianInt.toComplex x = 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) :
GaussianInt.toComplex x = { re := x.re, im := x.im }
@[simp]
theorem GaussianInt.to_real_re (x : GaussianInt) :
x.re = (GaussianInt.toComplex x).re
@[simp]
theorem GaussianInt.to_real_im (x : GaussianInt) :
x.im = (GaussianInt.toComplex x).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
theorem GaussianInt.toComplex_add (x : GaussianInt) (y : GaussianInt) :
GaussianInt.toComplex (x + y) = GaussianInt.toComplex x + GaussianInt.toComplex y
theorem GaussianInt.toComplex_mul (x : GaussianInt) (y : GaussianInt) :
GaussianInt.toComplex (x * y) = GaussianInt.toComplex x * GaussianInt.toComplex y
theorem GaussianInt.toComplex_one :
GaussianInt.toComplex 1 = 1
theorem GaussianInt.toComplex_zero :
GaussianInt.toComplex 0 = 0
theorem GaussianInt.toComplex_neg (x : GaussianInt) :
GaussianInt.toComplex (-x) = -GaussianInt.toComplex x
theorem GaussianInt.toComplex_sub (x : GaussianInt) (y : GaussianInt) :
GaussianInt.toComplex (x - y) = GaussianInt.toComplex x - GaussianInt.toComplex y
@[simp]
theorem GaussianInt.toComplex_star (x : GaussianInt) :
GaussianInt.toComplex (star x) = () (GaussianInt.toComplex x)
@[simp]
theorem GaussianInt.toComplex_inj {x : GaussianInt} {y : GaussianInt} :
GaussianInt.toComplex x = GaussianInt.toComplex y x = y
@[simp]
theorem GaussianInt.toComplex_eq_zero {x : GaussianInt} :
GaussianInt.toComplex x = 0 x = 0
@[simp]
theorem GaussianInt.intCast_real_norm (x : GaussianInt) :
() = Complex.normSq (GaussianInt.toComplex x)
@[deprecated GaussianInt.intCast_real_norm]
theorem GaussianInt.int_cast_real_norm (x : GaussianInt) :
() = Complex.normSq (GaussianInt.toComplex x)

Alias of GaussianInt.intCast_real_norm.

@[simp]
theorem GaussianInt.intCast_complex_norm (x : GaussianInt) :
() = (Complex.normSq (GaussianInt.toComplex x))
@[deprecated GaussianInt.intCast_complex_norm]
theorem GaussianInt.int_cast_complex_norm (x : GaussianInt) :
() = (Complex.normSq (GaussianInt.toComplex x))

Alias of GaussianInt.intCast_complex_norm.

@[simp]
theorem GaussianInt.abs_natCast_norm (x : GaussianInt) :
().natAbs =
@[deprecated GaussianInt.abs_natCast_norm]
theorem GaussianInt.abs_coe_nat_norm (x : GaussianInt) :
().natAbs =

Alias of GaussianInt.abs_natCast_norm.

@[simp]
theorem GaussianInt.natCast_natAbs_norm {α : Type u_1} [Ring α] (x : GaussianInt) :
().natAbs = ()
@[deprecated GaussianInt.natCast_natAbs_norm]
theorem GaussianInt.nat_cast_natAbs_norm {α : Type u_1} [Ring α] (x : GaussianInt) :
().natAbs = ()

Alias of GaussianInt.natCast_natAbs_norm.

theorem GaussianInt.natAbs_norm_eq (x : GaussianInt) :
().natAbs = x.re.natAbs * x.re.natAbs + x.im.natAbs * x.im.natAbs
Equations
theorem GaussianInt.div_def (x : GaussianInt) (y : GaussianInt) :
x / y = { re := round ((x * star y).re / ()), im := round ((x * star y).im / ()) }
theorem GaussianInt.toComplex_div_re (x : GaussianInt) (y : GaussianInt) :
(GaussianInt.toComplex (x / y)).re = (round (GaussianInt.toComplex x / GaussianInt.toComplex y).re)
theorem GaussianInt.toComplex_div_im (x : GaussianInt) (y : GaussianInt) :
(GaussianInt.toComplex (x / y)).im = (round (GaussianInt.toComplex x / GaussianInt.toComplex 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|) :
Complex.normSq x Complex.normSq y
theorem GaussianInt.normSq_div_sub_div_lt_one (x : GaussianInt) (y : GaussianInt) :
Complex.normSq (GaussianInt.toComplex x / GaussianInt.toComplex y - GaussianInt.toComplex (x / y)) < 1
Equations
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.natAbs_norm_mod_lt (x : GaussianInt) {y : GaussianInt} (hy : y 0) :
(Zsqrtd.norm (x % y)).natAbs < ().natAbs
theorem GaussianInt.norm_le_norm_mul_left (x : GaussianInt) {y : GaussianInt} (hy : y 0) :
().natAbs (Zsqrtd.norm (x * y)).natAbs
Equations
Equations
• One or more equations did not get rendered due to their size.
theorem GaussianInt.sq_add_sq_of_nat_prime_of_not_irreducible (p : ) [hp : Fact ()] (hpi : ¬) :
∃ (a : ) (b : ), a ^ 2 + b ^ 2 = p