theorem GaussInt.ext_iff {x : GaussInt} {y : GaussInt} : x = y ↔ x.re = y.re ∧ x.im = y.im

theorem GaussInt.ext {x : GaussInt} {y : GaussInt} (re : x.re = y.re) (im : x.im = y.im) : x = y

structure GaussInt : Type

• re : ℤ
• im : ℤ

instance GaussInt.instZero : Zero GaussInt

Equations

• GaussInt.instZero = { zero := { re := 0, im := 0 } }

instance GaussInt.instOne : One GaussInt

Equations

• GaussInt.instOne = { one := { re := 1, im := 0 } }

instance GaussInt.instAdd : Add GaussInt

Equations

• GaussInt.instAdd = { add := fun (x y : GaussInt) => { re := x.re + y.re, im := x.im + y.im } }

instance GaussInt.instNeg : Neg GaussInt

Equations

• GaussInt.instNeg = { neg := fun (x : GaussInt) => { re := -x.re, im := -x.im } }

instance GaussInt.instMul : Mul GaussInt

Equations

• GaussInt.instMul = { mul := fun (x y : GaussInt) => { re := x.re * y.re - x.im * y.im, im := x.re * y.im + x.im * y.re } }

theorem GaussInt.zero_def : 0 = { re := 0, im := 0 }

theorem GaussInt.one_def : 1 = { re := 1, im := 0 }

theorem GaussInt.add_def (x : GaussInt) (y : GaussInt) : x + y = { re := x.re + y.re, im := x.im + y.im }

theorem GaussInt.neg_def (x : GaussInt) : -x = { re := -x.re, im := -x.im }

theorem GaussInt.mul_def (x : GaussInt) (y : GaussInt) : x * y = { re := x.re * y.re - x.im * y.im, im := x.re * y.im + x.im * y.re }

@[simp]

theorem GaussInt.zero_re : GaussInt.re 0 = 0

@[simp]

theorem GaussInt.zero_im : GaussInt.im 0 = 0

@[simp]

theorem GaussInt.one_re : GaussInt.re 1 = 1

@[simp]

theorem GaussInt.one_im : GaussInt.im 1 = 0

@[simp]

theorem GaussInt.add_re (x : GaussInt) (y : GaussInt) : (x + y).re = x.re + y.re

@[simp]

theorem GaussInt.add_im (x : GaussInt) (y : GaussInt) : (x + y).im = x.im + y.im

@[simp]

theorem GaussInt.neg_re (x : GaussInt) : (-x).re = -x.re

@[simp]

theorem GaussInt.neg_im (x : GaussInt) : (-x).im = -x.im

@[simp]

theorem GaussInt.mul_re (x : GaussInt) (y : GaussInt) : (x * y).re = x.re * y.re - x.im * y.im

@[simp]

theorem GaussInt.mul_im (x : GaussInt) (y : GaussInt) : (x * y).im = x.re * y.im + x.im * y.re

instance GaussInt.instCommRing : CommRing GaussInt

Equations

• GaussInt.instCommRing = CommRing.mk GaussInt.instCommRing.proof_25

@[simp]

theorem GaussInt.sub_re (x : GaussInt) (y : GaussInt) : (x - y).re = x.re - y.re

@[simp]

theorem GaussInt.sub_im (x : GaussInt) (y : GaussInt) : (x - y).im = x.im - y.im

instance GaussInt.instNontrivial : Nontrivial GaussInt

Equations

• GaussInt.instNontrivial = ⋯

def Int.div' (a : ℤ) (b : ℤ) : ℤ

Equations

• a.div' b = (a + b / 2) / b

def Int.mod' (a : ℤ) (b : ℤ) : ℤ

Equations

• a.mod' b = (a + b / 2) % b - b / 2

theorem Int.div'_add_mod' (a : ℤ) (b : ℤ) : b * a.div' b + a.mod' b = a

theorem Int.abs_mod'_le (a : ℤ) (b : ℤ) (h : 0 < b) : |a.mod' b| ≤ b / 2

theorem Int.mod'_eq (a : ℤ) (b : ℤ) : a.mod' b = a - b * a.div' b

theorem sq_add_sq_eq_zero {α : Type u_1} [LinearOrderedRing α] (x : α) (y : α) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0

def GaussInt.norm (x : GaussInt) : ℤ

Equations

• x.norm = x.re ^ 2 + x.im ^ 2

@[simp]

theorem GaussInt.norm_nonneg (x : GaussInt) : 0 ≤ x.norm

theorem GaussInt.norm_eq_zero (x : GaussInt) : x.norm = 0 ↔ x = 0

theorem GaussInt.norm_pos (x : GaussInt) : 0 < x.norm ↔ x ≠ 0

theorem GaussInt.norm_mul (x : GaussInt) (y : GaussInt) : (x * y).norm = x.norm * y.norm

def GaussInt.conj (x : GaussInt) : GaussInt

Equations

• x.conj = { re := x.re, im := -x.im }

@[simp]

theorem GaussInt.conj_re (x : GaussInt) : x.conj.re = x.re

@[simp]

theorem GaussInt.conj_im (x : GaussInt) : x.conj.im = -x.im

theorem GaussInt.norm_conj (x : GaussInt) : x.conj.norm = x.norm

instance GaussInt.instDiv : Div GaussInt

Equations

• GaussInt.instDiv = { div := fun (x y : GaussInt) => { re := (x * y.conj).re.div' y.norm, im := (x * y.conj).im.div' y.norm } }

instance GaussInt.instMod : Mod GaussInt

Equations

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

theorem GaussInt.div_def (x : GaussInt) (y : GaussInt) : x / y = { re := (x * y.conj).re.div' y.norm, im := (x * y.conj).im.div' y.norm }

theorem GaussInt.mod_def (x : GaussInt) (y : GaussInt) : x % y = x - y * (x / y)

theorem GaussInt.norm_mod_lt (x : GaussInt) {y : GaussInt} (hy : y ≠ 0) : (x % y).norm < y.norm

theorem GaussInt.coe_natAbs_norm (x : GaussInt) : ↑x.norm.natAbs = x.norm

theorem GaussInt.natAbs_norm_mod_lt (x : GaussInt) (y : GaussInt) (hy : y ≠ 0) : (x % y).norm.natAbs < y.norm.natAbs

theorem GaussInt.not_norm_mul_left_lt_norm (x : GaussInt) {y : GaussInt} (hy : y ≠ 0) : ¬(x * y).norm.natAbs < x.norm.natAbs

instance GaussInt.instEuclideanDomain : EuclideanDomain GaussInt

Equations

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