Documentation

Mathlib.NumberTheory.Zsqrtd.GaussianInt

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.

See also #

See NumberTheory.Zsqrtd.QuadraticReciprocity for:

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.

@[reducible, inline]

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

Equations
Instances For
    Equations

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

    Equations
    Instances For
      theorem GaussianInt.toComplex_def (x : GaussianInt) :
      GaussianInt.toComplex x = x.re + x.im * Complex.I
      theorem GaussianInt.toComplex_def' (x : ) (y : ) :
      GaussianInt.toComplex { re := x, im := y } = x + y * Complex.I
      theorem GaussianInt.toComplex_def₂ (x : GaussianInt) :
      GaussianInt.toComplex x = { re := x.re, im := x.im }
      @[simp]
      theorem GaussianInt.to_real_re (x : GaussianInt) :
      x.re = (GaussianInt.toComplex x).re
      @[simp]
      theorem GaussianInt.to_real_im (x : GaussianInt) :
      x.im = (GaussianInt.toComplex x).im
      @[simp]
      theorem GaussianInt.toComplex_re (x : ) (y : ) :
      (GaussianInt.toComplex { re := x, im := y }).re = x
      @[simp]
      theorem GaussianInt.toComplex_im (x : ) (y : ) :
      (GaussianInt.toComplex { re := x, im := y }).im = y
      theorem GaussianInt.toComplex_add (x : GaussianInt) (y : GaussianInt) :
      GaussianInt.toComplex (x + y) = GaussianInt.toComplex x + GaussianInt.toComplex y
      theorem GaussianInt.toComplex_mul (x : GaussianInt) (y : GaussianInt) :
      GaussianInt.toComplex (x * y) = GaussianInt.toComplex x * GaussianInt.toComplex y
      theorem GaussianInt.toComplex_one :
      GaussianInt.toComplex 1 = 1
      theorem GaussianInt.toComplex_zero :
      GaussianInt.toComplex 0 = 0
      theorem GaussianInt.toComplex_neg (x : GaussianInt) :
      GaussianInt.toComplex (-x) = -GaussianInt.toComplex x
      theorem GaussianInt.toComplex_sub (x : GaussianInt) (y : GaussianInt) :
      GaussianInt.toComplex (x - y) = GaussianInt.toComplex x - GaussianInt.toComplex y
      @[simp]
      theorem GaussianInt.toComplex_star (x : GaussianInt) :
      GaussianInt.toComplex (star x) = (starRingEnd ) (GaussianInt.toComplex x)
      @[simp]
      theorem GaussianInt.toComplex_inj {x : GaussianInt} {y : GaussianInt} :
      GaussianInt.toComplex x = GaussianInt.toComplex y x = y
      @[simp]
      theorem GaussianInt.toComplex_eq_zero {x : GaussianInt} :
      GaussianInt.toComplex x = 0 x = 0
      @[simp]
      theorem GaussianInt.intCast_real_norm (x : GaussianInt) :
      (Zsqrtd.norm x) = Complex.normSq (GaussianInt.toComplex x)
      @[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.

      @[simp]
      theorem GaussianInt.intCast_complex_norm (x : GaussianInt) :
      (Zsqrtd.norm x) = (Complex.normSq (GaussianInt.toComplex x))
      @[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.

      @[deprecated GaussianInt.abs_natCast_norm]

      Alias of GaussianInt.abs_natCast_norm.

      @[simp]
      theorem GaussianInt.natCast_natAbs_norm {α : Type u_1} [Ring α] (x : GaussianInt) :
      (Zsqrtd.norm x).natAbs = (Zsqrtd.norm x)
      @[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.

      theorem GaussianInt.natAbs_norm_eq (x : GaussianInt) :
      (Zsqrtd.norm x).natAbs = x.re.natAbs * x.re.natAbs + x.im.natAbs * x.im.natAbs
      Equations
      theorem GaussianInt.div_def (x : GaussianInt) (y : GaussianInt) :
      x / y = { re := round ((x * star y).re / (Zsqrtd.norm y)), im := round ((x * star y).im / (Zsqrtd.norm y)) }
      theorem GaussianInt.toComplex_div_re (x : GaussianInt) (y : GaussianInt) :
      (GaussianInt.toComplex (x / y)).re = (round (GaussianInt.toComplex x / GaussianInt.toComplex y).re)
      theorem GaussianInt.toComplex_div_im (x : GaussianInt) (y : GaussianInt) :
      (GaussianInt.toComplex (x / y)).im = (round (GaussianInt.toComplex x / GaussianInt.toComplex y).im)
      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
      theorem GaussianInt.normSq_div_sub_div_lt_one (x : GaussianInt) (y : GaussianInt) :
      Complex.normSq (GaussianInt.toComplex x / GaussianInt.toComplex y - GaussianInt.toComplex (x / y)) < 1
      Equations
      theorem GaussianInt.mod_def (x : GaussianInt) (y : GaussianInt) :
      x % y = x - y * (x / y)
      theorem GaussianInt.natAbs_norm_mod_lt (x : GaussianInt) {y : GaussianInt} (hy : y 0) :
      (Zsqrtd.norm (x % y)).natAbs < (Zsqrtd.norm y).natAbs
      theorem GaussianInt.norm_le_norm_mul_left (x : GaussianInt) {y : GaussianInt} (hy : y 0) :
      (Zsqrtd.norm x).natAbs (Zsqrtd.norm (x * y)).natAbs
      Equations
      • One or more equations did not get rendered due to their size.
      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