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

GaussianInt = ℤ√(-1)

Instances For

source

instance GaussianInt.instRepr :

Repr GaussianInt

Equations

GaussianInt.instRepr = { reprPrec := fun (x : GaussianInt) (x_1 : ℕ) => Std.Format.text "⟨" ++ repr x.re ++ Std.Format.text ", " ++ repr x.im ++ Std.Format.text "⟩" }

source

instance GaussianInt.instCommRing :

CommRing GaussianInt

Equations

GaussianInt.instCommRing = Zsqrtd.commRing

source

def GaussianInt.toComplex :

GaussianInt →+* ℂ

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

Equations

GaussianInt.toComplex = Zsqrtd.lift ⟨Complex.I, GaussianInt.toComplex.proof_1⟩

Instances For

source

instance GaussianInt.instCoeComplex :

Coe GaussianInt ℂ

Equations

GaussianInt.instCoeComplex = { coe := ⇑GaussianInt.toComplex }

source

theorem GaussianInt.toComplex_def (x : GaussianInt) :

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

source

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

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

source

theorem GaussianInt.toComplex_def₂ (x : GaussianInt) :

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

source

@[simp]

theorem GaussianInt.to_real_re (x : GaussianInt) :

↑x.re = (GaussianInt.toComplex x).re

source

@[simp]

theorem GaussianInt.to_real_im (x : GaussianInt) :

↑x.im = (GaussianInt.toComplex x).im

source

@[simp]

theorem GaussianInt.toComplex_re (x y : ℤ) :

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

source

@[simp]

theorem GaussianInt.toComplex_im (x y : ℤ) :

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

source

theorem GaussianInt.toComplex_add (x y : GaussianInt) :

GaussianInt.toComplex (x + y) = GaussianInt.toComplex x + GaussianInt.toComplex y

source

theorem GaussianInt.toComplex_mul (x y : GaussianInt) :

GaussianInt.toComplex (x * y) = GaussianInt.toComplex x * GaussianInt.toComplex y

source

theorem GaussianInt.toComplex_one :

GaussianInt.toComplex 1 = 1

source

theorem GaussianInt.toComplex_zero :

GaussianInt.toComplex 0 = 0

source

theorem GaussianInt.toComplex_neg (x : GaussianInt) :

GaussianInt.toComplex (-x) = -GaussianInt.toComplex x

source

theorem GaussianInt.toComplex_sub (x y : GaussianInt) :

GaussianInt.toComplex (x - y) = GaussianInt.toComplex x - GaussianInt.toComplex y

source

@[simp]

theorem GaussianInt.toComplex_star (x : GaussianInt) :

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

source

@[simp]

theorem GaussianInt.toComplex_inj {x y : GaussianInt} :

GaussianInt.toComplex x = GaussianInt.toComplex y ↔ x = y

source

theorem GaussianInt.toComplex_injective :

Function.Injective ⇑GaussianInt.toComplex

source

@[simp]

theorem GaussianInt.toComplex_eq_zero {x : GaussianInt} :

GaussianInt.toComplex x = 0 ↔ x = 0

source

@[simp]

theorem GaussianInt.intCast_real_norm (x : GaussianInt) :

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

source

@[deprecated GaussianInt.intCast_real_norm]

theorem GaussianInt.int_cast_real_norm (x : GaussianInt) :

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

Alias of GaussianInt.intCast_real_norm.

source

@[simp]

theorem GaussianInt.intCast_complex_norm (x : GaussianInt) :

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

source

@[deprecated GaussianInt.intCast_complex_norm]

theorem GaussianInt.int_cast_complex_norm (x : GaussianInt) :

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

Alias of GaussianInt.intCast_complex_norm.

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

@[deprecated GaussianInt.abs_natCast_norm]

theorem GaussianInt.abs_coe_nat_norm (x : GaussianInt) :

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

Alias of GaussianInt.abs_natCast_norm.

source

@[simp]

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

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

source

@[deprecated GaussianInt.natCast_natAbs_norm]

theorem GaussianInt.nat_cast_natAbs_norm {α : Type u_1} [Ring α] (x : GaussianInt) :

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

Alias of GaussianInt.natCast_natAbs_norm.

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

GaussianInt.instDiv = { div := fun (x y : GaussianInt) => let n := (↑(Zsqrtd.norm y))⁻¹; let c := star y; { re := round (↑(x * c).re * n), im := round (↑(x * c).im * n) } }

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

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

source

theorem GaussianInt.toComplex_div_im (x y : GaussianInt) :

(GaussianInt.toComplex (x / y)).im = ↑(round (GaussianInt.toComplex x / GaussianInt.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 (GaussianInt.toComplex x / GaussianInt.toComplex y - GaussianInt.toComplex (x / y)) < 1

source

instance GaussianInt.instMod :

Mod GaussianInt

Equations

GaussianInt.instMod = { mod := fun (x y : GaussianInt) => x - y * (x / y) }

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

Equations

GaussianInt.instNontrivial = ⋯

source

instance GaussianInt.instEuclideanDomain :

EuclideanDomain GaussianInt

Equations

One or more equations did not get rendered due to their size.

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 #