structure Hurwitz : Type

• re : ℤ
• im_o : ℤ
• im_i : ℤ
• im_oi : ℤ

theorem Hurwitz.ext_iff {x y : 𝓞} : x = y ↔ x.re = y.re ∧ x.im_o = y.im_o ∧ x.im_i = y.im_i ∧ x.im_oi = y.im_oi

theorem Hurwitz.ext {x y : 𝓞} (re : x.re = y.re) (im_o : x.im_o = y.im_o) (im_i : x.im_i = y.im_i) (im_oi : x.im_oi = y.im_oi) : x = y

def term𝓞 : Lean.ParserDescr

noncomputable def Hurwitz.toQuaternion (z : 𝓞) : Quaternion ℝ

noncomputable def Hurwitz.fromQuaternion (z : Quaternion ℝ) : 𝓞

theorem Hurwitz.leftInverse_fromQuaternion_toQuaternion : Function.LeftInverse fromQuaternion toQuaternion

theorem Hurwitz.toQuaternion_injective : Function.Injective toQuaternion

theorem Hurwitz.leftInvOn_toQuaternion_fromQuaternion : Set.LeftInvOn toQuaternion fromQuaternion {q : Quaternion ℝ | ∃ (a : ℤ) (b : ℤ) (c : ℤ) (d : ℤ), q = { re := ↑a, imI := ↑b, imJ := ↑c, imK := ↑d } ∨ q = { re := ↑a + 2⁻¹, imI := ↑b + 2⁻¹, imJ := ↑c + 2⁻¹, imK := ↑d + 2⁻¹ }}

theorem Hurwitz.fromQuaternion_injOn : Set.InjOn fromQuaternion {q : Quaternion ℝ | ∃ (a : ℤ) (b : ℤ) (c : ℤ) (d : ℤ), q = { re := ↑a, imI := ↑b, imJ := ↑c, imK := ↑d } ∨ q = { re := ↑a + 2⁻¹, imI := ↑b + 2⁻¹, imJ := ↑c + 2⁻¹, imK := ↑d + 2⁻¹ }}

zero (0)

def Hurwitz.zero : 𝓞

The Hurwitz number 0

instance Hurwitz.instZero : Zero 𝓞

notation 0 for zero

@[simp]

theorem Hurwitz.zero_re : re 0 = 0

@[simp]

theorem Hurwitz.zero_im_o : im_o 0 = 0

@[simp]

theorem Hurwitz.zero_im_i : im_i 0 = 0

@[simp]

theorem Hurwitz.zero_im_oi : im_oi 0 = 0

theorem Hurwitz.toQuaternion_zero : toQuaternion 0 = 0

@[simp]

theorem Hurwitz.toQuaternion_eq_zero_iff {z : 𝓞} : z.toQuaternion = 0 ↔ z = 0

theorem Hurwitz.toQuaternion_ne_zero_iff {z : 𝓞} : z.toQuaternion ≠ 0 ↔ z ≠ 0

one (1)

def Hurwitz.one : 𝓞

instance Hurwitz.instOne : One 𝓞

Notation 1 for one

@[simp]

theorem Hurwitz.one_re : re 1 = 1

@[simp]

theorem Hurwitz.one_im_o : im_o 1 = 0

@[simp]

theorem Hurwitz.one_im_i : im_i 1 = 0

@[simp]

theorem Hurwitz.one_im_oi : im_oi 1 = 0

theorem Hurwitz.toQuaternion_one : toQuaternion 1 = 1

Neg (-)

def Hurwitz.neg (z : 𝓞) : 𝓞

The negation -z of a Hurwitz number

instance Hurwitz.instNeg : Neg 𝓞

Notation - for negation

@[simp]

theorem Hurwitz.neg_re (z : 𝓞) : (-z).re = -z.re

@[simp]

theorem Hurwitz.neg_im_o (z : 𝓞) : (-z).im_o = -z.im_o

@[simp]

theorem Hurwitz.neg_im_i (z : 𝓞) : (-z).im_i = -z.im_i

@[simp]

theorem Hurwitz.neg_im_oi (z : 𝓞) : (-z).im_oi = -z.im_oi

theorem Hurwitz.toQuaternion_neg (z : 𝓞) : (-z).toQuaternion = -z.toQuaternion

add (+)

def Hurwitz.add (z w : 𝓞) : 𝓞

addition z+w of complex numbers

instance Hurwitz.instAdd : Add 𝓞

Notation + for addition

@[simp]

theorem Hurwitz.add_re (z w : 𝓞) : (z + w).re = z.re + w.re

@[simp]

theorem Hurwitz.add_im_o (z w : 𝓞) : (z + w).im_o = z.im_o + w.im_o

@[simp]

theorem Hurwitz.add_im_i (z w : 𝓞) : (z + w).im_i = z.im_i + w.im_i

@[simp]

theorem Hurwitz.add_im_oi (z w : 𝓞) : (z + w).im_oi = z.im_oi + w.im_oi

theorem Hurwitz.toQuaternion_add (z w : 𝓞) : (z + w).toQuaternion = z.toQuaternion + w.toQuaternion

instance Hurwitz.instSub : Sub 𝓞

Notation + for addition

theorem Hurwitz.toQuaternion_sub (z w : 𝓞) : (z - w).toQuaternion = z.toQuaternion - w.toQuaternion

instance Hurwitz.instSMulNat : SMul ℕ 𝓞

theorem Hurwitz.preserves_nsmulRec {M : Type u_1} {N : Type u_2} [Zero M] [Add M] [AddMonoid N] (f : M → N) (zero : f 0 = 0) (add : ∀ (x y : M), f (x + y) = f x + f y) (n : ℕ) (x : M) : f (nsmulRec n x) = n • f x

theorem Hurwitz.toQuaternion_nsmul (z : 𝓞) (n : ℕ) : (n • z).toQuaternion = n • z.toQuaternion

instance Hurwitz.instSMulInt : SMul ℤ 𝓞

theorem Hurwitz.preserves_zsmul {G : Type u_1} {H : Type u_2} [Zero G] [Add G] [Neg G] [SMul ℕ G] [SubNegMonoid H] (f : G → H) (nsmul : ∀ (g : G) (n : ℕ), f (n • g) = n • f g) (neg : ∀ (x : G), f (-x) = -f x) (z : ℤ) (g : G) : f (zsmulRec (fun (x1 : ℕ) (x2 : G) => x1 • x2) z g) = z • f g

theorem Hurwitz.toQuaternion_zsmul (z : 𝓞) (n : ℤ) : (n • z).toQuaternion = n • z.toQuaternion

mul (*)

def Hurwitz.mul (z w : 𝓞) : 𝓞

Multiplication z*w of two Hurwitz numbers

instance Hurwitz.instMul : Mul 𝓞

Notation * for multiplication

@[simp]

theorem Hurwitz.mul_re (z w : 𝓞) : (z * w).re = z.re * w.re - z.im_o * w.im_o - z.im_i * w.im_o - z.im_i * w.im_i + z.im_i * w.im_oi - z.im_oi * w.im_oi

@[simp]

theorem Hurwitz.mul_im_o (z w : 𝓞) : (z * w).im_o = z.im_o * w.re + z.re * w.im_o - z.im_o * w.im_o - z.im_oi * w.im_o - z.im_oi * w.im_i + z.im_i * w.im_oi

@[simp]

theorem Hurwitz.mul_im_i (z w : 𝓞) : (z * w).im_i = z.im_i * w.re - z.im_i * w.im_o + z.im_oi * w.im_o + z.re * w.im_i - z.im_o * w.im_oi - z.im_i * w.im_oi

@[simp]

theorem Hurwitz.mul_im_oi (z w : 𝓞) : (z * w).im_oi = z.im_oi * w.re - z.im_i * w.im_o + z.im_o * w.im_i + z.re * w.im_oi - z.im_o * w.im_oi - z.im_oi * w.im_oi

theorem Hurwitz.toQuaternion_mul (z w : 𝓞) : (z * w).toQuaternion = z.toQuaternion * w.toQuaternion

theorem Hurwitz.o_mul_i : { re := 0, im_o := 1, im_i := 0, im_oi := 0 } * { re := 0, im_o := 0, im_i := 1, im_oi := 0 } = { re := 0, im_o := 0, im_i := 0, im_oi := 1 }

instance Hurwitz.instPowNat : Pow 𝓞 ℕ

theorem Hurwitz.preserves_npowRec {M : Type u_1} {N : Type u_2} [One M] [Mul M] [Monoid N] (f : M → N) (one : f 1 = 1) (mul : ∀ (x y : M), f (x * y) = f x * f y) (z : M) (n : ℕ) : f (npowRec n z) = f z ^ n

theorem Hurwitz.toQuaternion_npow (z : 𝓞) (n : ℕ) : (z ^ n).toQuaternion = z.toQuaternion ^ n

instance Hurwitz.instNatCast : NatCast 𝓞

theorem Hurwitz.preserves_unaryCast {R : Type u_1} {S : Type u_2} [One R] [Zero R] [Add R] [AddMonoidWithOne S] (f : R → S) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : R), f (x + y) = f x + f y) (n : ℕ) : f n.unaryCast = ↑n

theorem Hurwitz.toQuaternion_natCast (n : ℕ) : (↑n).toQuaternion = ↑n

instance Hurwitz.instIntCast : IntCast 𝓞

theorem Hurwitz.Int.castDef_ofNat {R : Type u_1} [NatCast R] [Neg R] (n : ℕ) : (Int.ofNat n).castDef = ↑n

theorem Hurwitz.Int.castDef_negSucc {R : Type u_1} [NatCast R] [Neg R] (n : ℕ) : (Int.negSucc n).castDef = -↑(n + 1)

theorem Hurwitz.preserves_castDef {R : Type u_1} {S : Type u_2} [NatCast R] [Neg R] [AddGroupWithOne S] (f : R → S) (natCast : ∀ (n : ℕ), f ↑n = ↑n) (neg : ∀ (x : R), f (-x) = -f x) (n : ℤ) : f n.castDef = ↑n

theorem Hurwitz.toQuaternion_intCast (n : ℤ) : (↑n).toQuaternion = ↑n

noncomputable instance Hurwitz.ring : Ring 𝓞

@[simp]

theorem Hurwitz.natCast_re (n : ℕ) : (↑n).re = ↑n

@[simp]

theorem Hurwitz.natCast_im_o (n : ℕ) : (↑n).im_o = 0

@[simp]

theorem Hurwitz.natCast_im_i (n : ℕ) : (↑n).im_i = 0

@[simp]

theorem Hurwitz.natCast_im_oi (n : ℕ) : (↑n).im_oi = 0

@[simp]

theorem Hurwitz.intCast_re (n : ℤ) : (↑n).re = n

@[simp]

theorem Hurwitz.intCast_im_o (n : ℤ) : (↑n).im_o = 0

@[simp]

theorem Hurwitz.intCast_im_i (n : ℤ) : (↑n).im_i = 0

@[simp]

theorem Hurwitz.intCast_im_oi (n : ℤ) : (↑n).im_oi = 0

instance Hurwitz.starRing : StarRing 𝓞

Conjugate; sends $a+bi+cj+dk$ to $a-bi-cj-dk$.

@[simp]

theorem Hurwitz.star_re (z : 𝓞) : (star z).re = z.re - z.im_o - z.im_oi

@[simp]

theorem Hurwitz.star_im_o (z : 𝓞) : (star z).im_o = -z.im_o

@[simp]

theorem Hurwitz.star_im_i (z : 𝓞) : (star z).im_i = -z.im_i

@[simp]

theorem Hurwitz.star_im_oi (z : 𝓞) : (star z).im_oi = -z.im_oi

theorem Hurwitz.toQuaternion_star (z : 𝓞) : (star z).toQuaternion = star z.toQuaternion

theorem Hurwitz.star_eq (z : 𝓞) : star z = (fromQuaternion ∘ star ∘ toQuaternion) z

instance Hurwitz.instCharZero : CharZero 𝓞

def Hurwitz.norm (z : 𝓞) : ℤ

theorem Hurwitz.norm_eq_mul_conj (z : 𝓞) : ↑z.norm = z * star z

theorem Hurwitz.coe_norm (z : 𝓞) : ↑z.norm = (↑z.re - 2⁻¹ * ↑z.im_o - 2⁻¹ * ↑z.im_oi) ^ 2 + (↑z.im_i + 2⁻¹ * ↑z.im_o - 2⁻¹ * ↑z.im_oi) ^ 2 + (2⁻¹ * ↑z.im_o + 2⁻¹ * ↑z.im_oi) ^ 2 + (2⁻¹ * ↑z.im_o - 2⁻¹ * ↑z.im_oi) ^ 2

theorem Hurwitz.norm_zero : norm 0 = 0

theorem Hurwitz.norm_one : norm 1 = 1

theorem Hurwitz.norm_mul (x y : 𝓞) : (x * y).norm = x.norm * y.norm

theorem Hurwitz.norm_nonneg (x : 𝓞) : 0 ≤ x.norm

theorem Hurwitz.norm_eq_zero (x : 𝓞) : x.norm = 0 ↔ x = 0

theorem Hurwitz.normSq_toQuaternion (z : 𝓞) : Quaternion.normSq z.toQuaternion = ↑z.norm

theorem Hurwitz.exists_near (a : Quaternion ℝ) : ∃ (q : 𝓞), dist a q.toQuaternion < 1

theorem Hurwitz.quot_rem (a b : 𝓞) (hb : b ≠ 0) : ∃ (q : 𝓞) (r : 𝓞), a = q * b + r ∧ r.norm < b.norm

theorem Hurwitz.left_ideal_princ (I : Submodule 𝓞 𝓞) : ∃ (a : 𝓞), I = 𝓞 ∙ a