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.

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.

source

@[reducible, inline]

abbrev GaussianInt :

Type

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

Equations

Instances For

source

instance GaussianInt.instRepr :

Repr GaussianInt

Equations

source

instance GaussianInt.instCommRing :

CommRing GaussianInt

Equations

source

def GaussianInt.toComplex :

GaussianInt →+* ℂ

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

Equations

Instances For

source

instance GaussianInt.instCoeComplex :

Coe GaussianInt ℂ

Equations

source

theorem GaussianInt.toComplex_def (x : GaussianInt) :

toComplex x = ↑x.re + ↑x.im * Complex.I

source

theorem GaussianInt.toComplex_def' (x y : ℤ) :

toComplex { re := x, im := y } = ↑x + ↑y * Complex.I

source

theorem GaussianInt.toComplex_def₂ (x : GaussianInt) :

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

source

@[simp]

theorem GaussianInt.to_real_re (x : GaussianInt) :

↑x.re = (toComplex x).re

source

@[simp]

theorem GaussianInt.to_real_im (x : GaussianInt) :

↑x.im = (toComplex x).im

source

@[simp]

theorem GaussianInt.toComplex_re (x y : ℤ) :

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

source

@[simp]

theorem GaussianInt.toComplex_im (x y : ℤ) :

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

source

theorem GaussianInt.toComplex_add (x y : GaussianInt) :

toComplex (x + y) = toComplex x + toComplex y

source

theorem GaussianInt.toComplex_mul (x y : GaussianInt) :

toComplex (x * y) = toComplex x * toComplex y

source

theorem GaussianInt.toComplex_one :

toComplex 1 = 1

source

theorem GaussianInt.toComplex_zero :

toComplex 0 = 0

source

theorem GaussianInt.toComplex_neg (x : GaussianInt) :

toComplex (-x) = -toComplex x

source

theorem GaussianInt.toComplex_sub (x y : GaussianInt) :

toComplex (x - y) = toComplex x - toComplex y

source

@[simp]

theorem GaussianInt.toComplex_star (x : GaussianInt) :

toComplex (star x) = (starRingEnd ℂ) (toComplex x)

source

@[simp]

theorem GaussianInt.toComplex_inj {x y : GaussianInt} :

toComplex x = toComplex y ↔ x = y

source

theorem GaussianInt.toComplex_injective :

Function.Injective ⇑toComplex

source

@[simp]

theorem GaussianInt.toComplex_eq_zero {x : GaussianInt} :

toComplex x = 0 ↔ x = 0

source

@[simp]

theorem GaussianInt.intCast_real_norm (x : GaussianInt) :

↑(Zsqrtd.norm x) = Complex.normSq (toComplex x)

source

@[simp]

theorem GaussianInt.intCast_complex_norm (x : GaussianInt) :

↑(Zsqrtd.norm x) = ↑(Complex.normSq (toComplex x))

source

theorem GaussianInt.norm_nonneg (x : GaussianInt) :

0 ≤ Zsqrtd.norm x

source

@[simp]

theorem GaussianInt.norm_eq_zero {x : GaussianInt} :

Zsqrtd.norm x = 0 ↔ x = 0

source

theorem GaussianInt.norm_pos {x : GaussianInt} :

0 < Zsqrtd.norm x ↔ x ≠ 0

source

theorem GaussianInt.abs_natCast_norm (x : GaussianInt) :

↑(Zsqrtd.norm x).natAbs = Zsqrtd.norm x

source

theorem GaussianInt.natCast_natAbs_norm {α : Type u_1} [AddGroupWithOne α] (x : GaussianInt) :

↑(Zsqrtd.norm x).natAbs = ↑(Zsqrtd.norm x)

source

theorem GaussianInt.natAbs_norm_eq (x : GaussianInt) :

(Zsqrtd.norm x).natAbs = x.re.natAbs * x.re.natAbs + x.im.natAbs * x.im.natAbs

source

instance GaussianInt.instDiv :

Div GaussianInt

Equations

source

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)) }

source

theorem GaussianInt.toComplex_div_re (x y : GaussianInt) :

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

source

theorem GaussianInt.toComplex_div_im (x y : GaussianInt) :

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

source

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

source

theorem GaussianInt.normSq_div_sub_div_lt_one (x y : GaussianInt) :

Complex.normSq (toComplex x / toComplex y - toComplex (x / y)) < 1

source

instance GaussianInt.instMod :

Mod GaussianInt

Equations

source

theorem GaussianInt.mod_def (x y : GaussianInt) :

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

source

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

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

source

theorem GaussianInt.natAbs_norm_mod_lt (x : GaussianInt) {y : GaussianInt} (hy : y ≠ 0) :

(Zsqrtd.norm (x % y)).natAbs < (Zsqrtd.norm y).natAbs

source

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

(Zsqrtd.norm x).natAbs ≤ (Zsqrtd.norm (x * y)).natAbs

source

instance GaussianInt.instNontrivial :

Nontrivial GaussianInt

source

instance GaussianInt.instEuclideanDomain :

EuclideanDomain GaussianInt

Equations

source

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

Documentation

Mathlib.NumberTheory.Zsqrtd.GaussianInt

Gaussian integers #

Main definitions #

See also #

Notations #

Implementation notes #