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 also

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

Notation

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]

abbrev GaussianInt : Type

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

instance GaussianInt.instRepr : Repr GaussianInt

instance GaussianInt.instCommRing : CommRing GaussianInt

def GaussianInt.toComplex : GaussianInt →+* ℂ

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

instance GaussianInt.instCoeComplex : Coe GaussianInt ℂ

theorem GaussianInt.toComplex_def (x : GaussianInt) : toComplex x = ↑x.re + ↑x.im * Complex.I

theorem GaussianInt.toComplex_def' (x y : ℤ) : toComplex { re := x, im := y } = ↑x + ↑y * Complex.I

theorem GaussianInt.toComplex_def₂ (x : GaussianInt) : toComplex x = { re := ↑x.re, im := ↑x.im }

@[simp]

theorem GaussianInt.intCast_re (x : GaussianInt) : ↑x.re = (toComplex x).re

@[deprecated GaussianInt.intCast_re (since := "2025-08-31")]

theorem GaussianInt.to_real_re (x : GaussianInt) : ↑x.re = (toComplex x).re

Alias of GaussianInt.intCast_re.

@[simp]

theorem GaussianInt.intCast_im (x : GaussianInt) : ↑x.im = (toComplex x).im

@[deprecated GaussianInt.intCast_im (since := "2025-08-31")]

theorem GaussianInt.to_real_im (x : GaussianInt) : ↑x.im = (toComplex x).im

Alias of GaussianInt.intCast_im.

@[simp]

theorem GaussianInt.re_toComplex (x y : ℤ) : (toComplex { re := x, im := y }).re = ↑x

@[deprecated GaussianInt.re_toComplex (since := "2025-08-31")]

theorem GaussianInt.toComplex_re (x y : ℤ) : (toComplex { re := x, im := y }).re = ↑x

Alias of GaussianInt.re_toComplex.

@[simp]

theorem GaussianInt.im_toComplex (x y : ℤ) : (toComplex { re := x, im := y }).im = ↑y

@[deprecated GaussianInt.im_toComplex (since := "2025-08-31")]

theorem GaussianInt.toComplex_im (x y : ℤ) : (toComplex { re := x, im := y }).im = ↑y

Alias of GaussianInt.im_toComplex.

theorem GaussianInt.toComplex_add (x y : GaussianInt) : toComplex (x + y) = toComplex x + toComplex y

theorem GaussianInt.toComplex_mul (x y : GaussianInt) : toComplex (x * y) = toComplex x * toComplex y

theorem GaussianInt.toComplex_one : toComplex 1 = 1

theorem GaussianInt.toComplex_zero : toComplex 0 = 0

theorem GaussianInt.toComplex_neg (x : GaussianInt) : toComplex (-x) = -toComplex x

theorem GaussianInt.toComplex_sub (x y : GaussianInt) : toComplex (x - y) = toComplex x - toComplex y

@[simp]

theorem GaussianInt.toComplex_star (x : GaussianInt) : toComplex (star x) = (starRingEnd ℂ) (toComplex x)

@[simp]

theorem GaussianInt.toComplex_inj {x y : GaussianInt} : toComplex x = toComplex y ↔ x = y

theorem GaussianInt.toComplex_injective : Function.Injective ⇑toComplex

@[simp]

theorem GaussianInt.toComplex_eq_zero {x : GaussianInt} : toComplex x = 0 ↔ x = 0

@[simp]

theorem GaussianInt.intCast_real_norm (x : GaussianInt) : ↑(Zsqrtd.norm x) = Complex.normSq (toComplex x)

@[simp]

theorem GaussianInt.intCast_complex_norm (x : GaussianInt) : ↑(Zsqrtd.norm x) = ↑(Complex.normSq (toComplex x))

theorem GaussianInt.norm_nonneg (x : GaussianInt) : 0 ≤ Zsqrtd.norm x

@[simp]

theorem GaussianInt.norm_eq_zero {x : GaussianInt} : Zsqrtd.norm x = 0 ↔ x = 0

theorem GaussianInt.norm_pos {x : GaussianInt} : 0 < Zsqrtd.norm x ↔ x ≠ 0

theorem GaussianInt.abs_natCast_norm (x : GaussianInt) : ↑(Zsqrtd.norm x).natAbs = Zsqrtd.norm x

theorem GaussianInt.natCast_natAbs_norm {α : Type u_1} [AddGroupWithOne α] (x : GaussianInt) : ↑(Zsqrtd.norm x).natAbs = ↑(Zsqrtd.norm x)

theorem GaussianInt.natAbs_norm_eq (x : GaussianInt) : (Zsqrtd.norm x).natAbs = x.re.natAbs * x.re.natAbs + x.im.natAbs * x.im.natAbs

instance GaussianInt.instDiv : Div GaussianInt

theorem GaussianInt.div_def (x y : GaussianInt) : x / y = { re := round (↑(x * star y).re / ↑(Zsqrtd.norm y)), im := round (↑(x * star y).im / ↑(Zsqrtd.norm y)) }

theorem GaussianInt.toComplex_re_div (x y : GaussianInt) : (toComplex (x / y)).re = ↑(round (toComplex x / toComplex y).re)

@[deprecated GaussianInt.toComplex_re_div (since := "2025-08-31")]

theorem GaussianInt.toComplex_div_re (x y : GaussianInt) : (toComplex (x / y)).re = ↑(round (toComplex x / toComplex y).re)

Alias of GaussianInt.toComplex_re_div.

theorem GaussianInt.toComplex_im_div (x y : GaussianInt) : (toComplex (x / y)).im = ↑(round (toComplex x / toComplex y).im)

@[deprecated GaussianInt.toComplex_im_div (since := "2025-08-31")]

theorem GaussianInt.toComplex_div_im (x y : GaussianInt) : (toComplex (x / y)).im = ↑(round (toComplex x / toComplex y).im)

Alias of GaussianInt.toComplex_im_div.

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 y : GaussianInt) : Complex.normSq (toComplex x / toComplex y - toComplex (x / y)) < 1

instance GaussianInt.instMod : Mod GaussianInt

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

theorem GaussianInt.norm_mod_lt (x : GaussianInt) {y : GaussianInt} (hy : y ≠ 0) : Zsqrtd.norm (x % y) < Zsqrtd.norm y

theorem GaussianInt.natAbs_norm_mod_lt (x : GaussianInt) {y : GaussianInt} (hy : y ≠ 0) : (Zsqrtd.norm (x % y)).natAbs < (Zsqrtd.norm y).natAbs

theorem GaussianInt.norm_le_norm_mul_left (x : GaussianInt) {y : GaussianInt} (hy : y ≠ 0) : (Zsqrtd.norm x).natAbs ≤ (Zsqrtd.norm (x * y)).natAbs

instance GaussianInt.instNontrivial : Nontrivial GaussianInt

instance GaussianInt.instEuclideanDomain : EuclideanDomain GaussianInt

theorem GaussianInt.sq_add_sq_of_nat_prime_of_not_irreducible (p : ℕ) [hp : Fact (Nat.Prime p)] (hpi : ¬Irreducible ↑p) : ∃ (a : ℕ) (b : ℕ), a ^ 2 + b ^ 2 = p