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.

@[reducible]
def gaussian_int  :

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

Equations
@[protected, instance]
Equations

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

Equations
theorem gaussian_int.to_complex_def' (x y : ) :
{re := x, im := y} = x + y * complex.I
@[simp]
@[simp]
@[simp]
theorem gaussian_int.to_complex_re (x y : ) :
{re := x, im := y}.re = x
@[simp]
theorem gaussian_int.to_complex_im (x y : ) :
{re := x, im := y}.im = y
@[simp]
theorem gaussian_int.to_complex_add (x y : gaussian_int) :
(x + y) = x + y
@[simp]
theorem gaussian_int.to_complex_mul (x y : gaussian_int) :
(x * y) = x * y
@[simp]
@[simp]
@[simp]
theorem gaussian_int.to_complex_sub (x y : gaussian_int) :
(x - y) = x - y
@[simp]
@[simp]
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem gaussian_int.mod_def (x y : gaussian_int) :
x % y = x - y * (x / y)
@[protected, instance]
@[protected, instance]
Equations
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