mathlib3 documentation

number_theory.zsqrtd.gaussian_int

Gaussian integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

See also #

See number_theory.zsqrtd.gaussian_int for:

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
@[reducible]
def gaussian_int  :
Type

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

Equations
source
@[protected, instance]
def gaussian_int.has_repr  :
has_repr gaussian_int
Equations
source
@[protected, instance]
def gaussian_int.comm_ring  :
comm_ring gaussian_int
Equations
source
def gaussian_int.to_complex  :
gaussian_int →+* ℂ

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

Equations
source
@[protected, instance]
def gaussian_int.complex.has_coe  :
has_coe gaussian_int ℂ
Equations
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_star (x : gaussian_int) :
↑(has_star.star x) = ⇑(star_ring_end ℂ) ↑x
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
theorem gaussian_int.abs_coe_nat_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
source
theorem gaussian_int.div_def (x y : gaussian_int) :
x / y = {re := round (↑((x * has_star.star y).re) / ↑(zsqrtd.norm y)), im := round (↑((x * has_star.star 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
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
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