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.

source

def gaussian_int :

Type

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

Equations

gaussian_int = ℤ√-1

source

@[protected, instance]

def gaussian_int.has_repr :

has_repr gaussian_int

Equations

gaussian_int.has_repr = {repr := λ (x : gaussian_int), "⟨" ++ repr x.re ++ ", " ++ repr x.im ++ "⟩"}

source

@[protected, instance]

def gaussian_int.comm_ring :

comm_ring gaussian_int

Equations

gaussian_int.comm_ring = zsqrtd.comm_ring

source

def gaussian_int.to_complex :

gaussian_int →+* ℂ

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

Equations

gaussian_int.to_complex = ⇑zsqrtd.lift ⟨complex.I, gaussian_int.to_complex._proof_1⟩

source

@[protected, instance]

def gaussian_int.complex.has_coe :

has_coe gaussian_int ℂ

Equations

gaussian_int.complex.has_coe = {coe := ⇑gaussian_int.to_complex}

source

theorem gaussian_int.to_complex_def (x : gaussian_int) :

↑x = ↑(x.re) + (↑(x.im)) * complex.I

source

theorem gaussian_int.to_complex_def' (x y : ℤ) :

↑{re := x, im := y} = ↑x + (↑y) * complex.I

source

theorem gaussian_int.to_complex_def₂ (x : gaussian_int) :

↑x = {re := ↑(x.re), im := ↑(x.im)}

source

@[simp]

theorem gaussian_int.to_real_re (x : gaussian_int) :

↑(x.re) = ↑x.re

source

@[simp]

theorem gaussian_int.to_real_im (x : gaussian_int) :

↑(x.im) = ↑x.im

source

@[simp]

theorem gaussian_int.to_complex_re (x y : ℤ) :

↑{re := x, im := y}.re = ↑x

source

@[simp]

theorem gaussian_int.to_complex_im (x y : ℤ) :

↑{re := x, im := y}.im = ↑y

source

@[simp]

theorem gaussian_int.to_complex_add (x y : gaussian_int) :

↑(x + y) = ↑x + ↑y

source

@[simp]

theorem gaussian_int.to_complex_mul (x y : gaussian_int) :

↑x * y = (↑x) * ↑y

source

@[simp]

theorem gaussian_int.to_complex_one :

↑1 = 1

source

@[simp]

theorem gaussian_int.to_complex_zero :

↑0 = 0

source

@[simp]

theorem gaussian_int.to_complex_neg (x : gaussian_int) :

↑-x = -↑x

source

@[simp]

theorem gaussian_int.to_complex_sub (x y : gaussian_int) :

↑(x - y) = ↑x - ↑y

source

@[simp]

theorem gaussian_int.to_complex_inj {x y : gaussian_int} :

↑x = ↑y ↔ x = y

source

@[simp]

theorem gaussian_int.to_complex_eq_zero {x : gaussian_int} :

↑x = 0 ↔ x = 0

source

@[simp]

theorem gaussian_int.nat_cast_real_norm (x : gaussian_int) :

↑(zsqrtd.norm x) = ⇑complex.norm_sq ↑x

source

@[simp]

theorem gaussian_int.nat_cast_complex_norm (x : gaussian_int) :

↑(zsqrtd.norm x) = ↑(⇑complex.norm_sq ↑x)

source

theorem gaussian_int.norm_nonneg (x : gaussian_int) :

0 ≤ zsqrtd.norm x

source

@[simp]

theorem gaussian_int.norm_eq_zero {x : gaussian_int} :

zsqrtd.norm x = 0 ↔ x = 0

source

theorem gaussian_int.norm_pos {x : gaussian_int} :

0 < zsqrtd.norm x ↔ x ≠ 0

source

@[simp]

theorem gaussian_int.coe_nat_abs_norm (x : gaussian_int) :

↑((zsqrtd.norm x).nat_abs) = zsqrtd.norm x

source

@[simp]

theorem gaussian_int.nat_cast_nat_abs_norm {α : Type u_1} [ring α] (x : gaussian_int) :

↑((zsqrtd.norm x).nat_abs) = ↑(zsqrtd.norm x)

source

theorem gaussian_int.nat_abs_norm_eq (x : gaussian_int) :

(zsqrtd.norm x).nat_abs = (x.re.nat_abs) * x.re.nat_abs + (x.im.nat_abs) * x.im.nat_abs

source

@[protected, instance]

def gaussian_int.has_div :

has_div gaussian_int

Equations

gaussian_int.has_div = {div := λ (x y : gaussian_int), 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)}}

source

theorem gaussian_int.div_def (x y : gaussian_int) :

x / y = {re := round (↑((x * zsqrtd.conj y).re) / ↑(zsqrtd.norm y)), im := round (↑((x * zsqrtd.conj y).im) / ↑(zsqrtd.norm y))}

source

theorem gaussian_int.to_complex_div_re (x y : gaussian_int) :

↑(x / y).re = ↑(round (↑x / ↑y).re)

source

theorem gaussian_int.to_complex_div_im (x y : gaussian_int) :

↑(x / y).im = ↑(round (↑x / ↑y).im)

source

theorem gaussian_int.norm_sq_le_norm_sq_of_re_le_of_im_le {x y : ℂ} (hre : |x.re | ≤ |y.re |) (him : |x.im | ≤ |y.im |) :

⇑complex.norm_sq x ≤ ⇑complex.norm_sq y

source

theorem gaussian_int.norm_sq_div_sub_div_lt_one (x y : gaussian_int) :

⇑complex.norm_sq (↑x / ↑y - ↑(x / y)) < 1

source

@[protected, instance]

def gaussian_int.has_mod :

has_mod gaussian_int

Equations

gaussian_int.has_mod = {mod := λ (x y : gaussian_int), x - y * (x / y)}

source

theorem gaussian_int.mod_def (x y : gaussian_int) :

x % y = x - y * (x / y)

source

theorem gaussian_int.norm_mod_lt (x : gaussian_int) {y : gaussian_int} (hy : y ≠ 0) :

zsqrtd.norm (x % y) < zsqrtd.norm y

source

theorem gaussian_int.nat_abs_norm_mod_lt (x : gaussian_int) {y : gaussian_int} (hy : y ≠ 0) :

(zsqrtd.norm (x % y)).nat_abs < (zsqrtd.norm y).nat_abs

source

theorem gaussian_int.norm_le_norm_mul_left (x : gaussian_int) {y : gaussian_int} (hy : y ≠ 0) :

(zsqrtd.norm x).nat_abs ≤ (x * y).norm.nat_abs

source

@[protected, instance]

def gaussian_int.nontrivial :

nontrivial gaussian_int

source

@[protected, instance]

def gaussian_int.euclidean_domain :

euclidean_domain gaussian_int

Equations

gaussian_int.euclidean_domain = {to_comm_ring := {add := comm_ring.add gaussian_int.comm_ring, add_assoc := _, zero := comm_ring.zero gaussian_int.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul gaussian_int.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg gaussian_int.comm_ring, sub := comm_ring.sub gaussian_int.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul gaussian_int.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, 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 := _, npow := comm_ring.npow gaussian_int.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}, to_nontrivial := gaussian_int.euclidean_domain._proof_1, quotient := has_div.div gaussian_int.has_div, quotient_zero := gaussian_int.euclidean_domain._proof_2, remainder := has_mod.mod gaussian_int.has_mod, quotient_mul_add_remainder_eq := gaussian_int.euclidean_domain._proof_3, r := measure (int.nat_abs ∘ zsqrtd.norm), r_well_founded := gaussian_int.euclidean_domain._proof_4, remainder_lt := gaussian_int.nat_abs_norm_mod_lt, mul_left_not_lt := gaussian_int.euclidean_domain._proof_5}

source

theorem gaussian_int.mod_four_eq_three_of_nat_prime_of_prime (p : ℕ) [hp : fact (nat.prime p)] (hpi : prime ↑p) :

p % 4 = 3

source

theorem gaussian_int.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

source

theorem gaussian_int.prime_of_nat_prime_of_mod_four_eq_three (p : ℕ) [hp : fact (nat.prime p)] (hp3 : p % 4 = 3) :

prime ↑p

source

theorem gaussian_int.prime_iff_mod_four_eq_three_of_nat_prime (p : ℕ) [hp : fact (nat.prime p)] :

prime ↑p ↔ p % 4 = 3

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