Hurwitz.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

95 declarations, 0 contain sorry, 0 declared as axioms

Hurwitz integers

The ring of Hurwitz integers, the maximal order in the rational quaternions generated by 1, i, j, k together with ω := (-1 + i + j + k) / 2.

Main definitions

Hurwitz: the ring of Hurwitz integers, defined as a structure with an integer basis 1, ω, i, j.
Hurwitz.toQuaternion: the embedding into the rational quaternions.

Imports (1)

Mathlib.Analysis.Quaternion

Imported by 2 files

structure Hurwitz Hurwitz integers in the quaternions line 29 source
Source documentation
Hurwitz integers in the quaternions. ℤ-Basis 1, ω=(-1+i+j+k)/2, i and ωi=(-1-i+j-k)/2.

no axioms what this means
```
structure Hurwitz : Type where
…
```
def Hurwitz.toQuaternion The embedding of the Hurwitz integers into the rational quaternions line 45 source
Source documentation
The embedding of the Hurwitz integers into the rational quaternions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Quaternion, Real
Proof uses: QuaternionAlgebra.mk, Neg.neg, OfNat.ofNat, HSub.hSub, Hurwitz.re, HMul.hMul, Inv.inv, Hurwitz.imO, Hurwitz.imOI, HAdd.hAdd, Hurwitz.imI
20 instances, coercions and auxiliary constants left out.
```
noncomputable def toQuaternion (z : 𝓞) : ℍ where
…
```
def Hurwitz.fromQuaternion Rounds a quaternion to a nearby Hurwitz integer; serves as a left inverse to toQuaternion line 53 source
Source documentation
Rounds a quaternion to a nearby Hurwitz integer; serves as a left inverse to toQuaternion.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Quaternion, Real, Hurwitz
Proof uses: Hurwitz.mk, Int.floor, HAdd.hAdd, QuaternionAlgebra.re, Neg.neg, OfNat.ofNat, QuaternionAlgebra.imJ, QuaternionAlgebra.imK, HSub.hSub, QuaternionAlgebra.imI
15 instances, coercions and auxiliary constants left out.
```
noncomputable def fromQuaternion (z : ℍ) : 𝓞 where
…
```
lemma Hurwitz.leftInverse_fromQuaternion_toQuaternion line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.LeftInverse, Hurwitz, Quaternion, Real, Hurwitz.fromQuaternion, Hurwitz.toQuaternion
Proof uses: of_eq_true, Eq, Eq.trans, Hurwitz.mk, Hurwitz.re, Hurwitz.imO, Hurwitz.imI, Hurwitz.imOI, True, congrFun', congrArg, congr, Int, Int.floor, HAdd.hAdd, QuaternionAlgebra.re, Neg.neg, OfNat.ofNat, QuaternionAlgebra.imJ, QuaternionAlgebra.imK and 17 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.toQuaternion_injective line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Injective, Hurwitz, Quaternion, Real, Hurwitz.toQuaternion
Proof uses: Function.LeftInverse.injective, Hurwitz.fromQuaternion, Hurwitz.leftInverse_fromQuaternion_toQuaternion
6 instances, coercions and auxiliary constants left out.
lemma Hurwitz.leftInvOn_toQuaternion_fromQuaternion line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set.LeftInvOn, Quaternion, Real, Hurwitz, Hurwitz.toQuaternion, Hurwitz.fromQuaternion, Set.ofPred, Exists, Int, Or, Eq, QuaternionAlgebra.mk, Neg.neg, OfNat.ofNat, HAdd.hAdd, Inv.inv, Nat
Proof uses: Eq.mpr, HMul.hMul, inferInstance, CommGroupWithZero, id, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, List.nil, Prod, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, rfl, Eq.trans, Mathlib.Tactic.FieldSimp.subst_add, Eq.refl, Mathlib.Tactic.FieldSimp.NF.atom_eq_eval, Eq.symm, Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg, Mathlib.Meta.NormNum.isNat_eq_false and 93 more
126 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.fromQuaternion_injOn line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set.InjOn, Quaternion, Real, Hurwitz, Hurwitz.fromQuaternion, Set.ofPred, Exists, Int, Or, Eq, QuaternionAlgebra.mk, Neg.neg, OfNat.ofNat, HAdd.hAdd, Inv.inv, Nat
Proof uses: Set.LeftInvOn.injOn, Hurwitz.toQuaternion, Hurwitz.leftInvOn_toQuaternion_fromQuaternion
30 instances, coercions and auxiliary constants left out.
def Hurwitz.zero The Hurwitz number 0 line 96 source
Source documentation
The Hurwitz number 0

no axioms what this means
Statement uses: Hurwitz
Proof uses: Hurwitz.mk, OfNat.ofNat, Int
1 instances, coercions and auxiliary constants left out.
```
def zero : 𝓞 := ⟨0, 0, 0, 0⟩
```
instance Hurwitz.(instance at line 99) line 99 source
Source documentation
notation 0 for zero
```
instance : Zero 𝓞 := ⟨zero⟩
```
Mentions: Hurwitz.zero
lemma Hurwitz.zero_re line 101 source
no axioms what this means
Statement uses: Eq, Int, Hurwitz.re, OfNat.ofNat, Hurwitz
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
lemma Hurwitz.zero_im_o line 102 source
no axioms what this means
Statement uses: Eq, Int, Hurwitz.imO, OfNat.ofNat, Hurwitz
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
lemma Hurwitz.zero_im_i line 103 source
no axioms what this means
Statement uses: Eq, Int, Hurwitz.imI, OfNat.ofNat, Hurwitz
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
lemma Hurwitz.zero_im_oi line 104 source
no axioms what this means
Statement uses: Eq, Int, Hurwitz.imOI, OfNat.ofNat, Hurwitz
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
lemma Hurwitz.toQuaternion_zero line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Quaternion, Real, Hurwitz.toQuaternion, OfNat.ofNat, Hurwitz, Neg.neg
Proof uses: Quaternion.ext, of_eq_true, QuaternionAlgebra.re, Eq.trans, True, congrFun', congrArg, QuaternionAlgebra.mk, congr, QuaternionAlgebra, HSub.hSub, Hurwitz.re, HMul.hMul, Inv.inv, Hurwitz.imO, Hurwitz.imOI, HAdd.hAdd, Hurwitz.imI, Int.cast_zero, MulZeroClass.mul_zero and 6 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.toQuaternion_eq_zero_iff line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Iff, Eq, Quaternion, Real, Hurwitz.toQuaternion, OfNat.ofNat, Neg.neg
Proof uses: Function.Injective.eq_iff', Hurwitz.toQuaternion_injective, Hurwitz.toQuaternion_zero
14 instances, coercions and auxiliary constants left out.
lemma Hurwitz.toQuaternion_ne_zero_iff line 113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Iff, Ne, Quaternion, Real, Hurwitz.toQuaternion, OfNat.ofNat, Neg.neg
Proof uses: Function.Injective.ne_iff', Hurwitz.toQuaternion_injective, Hurwitz.toQuaternion_zero
14 instances, coercions and auxiliary constants left out.
def Hurwitz.one The Hurwitz number 1 line 119 source
Source documentation
The Hurwitz number 1.

no axioms what this means
Statement uses: Hurwitz
Proof uses: Hurwitz.mk, OfNat.ofNat, Int
1 instances, coercions and auxiliary constants left out.
```
def one : 𝓞 := ⟨1, 0, 0, 0⟩
```
instance Hurwitz.(instance at line 122) line 122 source
Source documentation
Notation 1 for one
```
instance : One 𝓞 := ⟨one⟩
```
Mentions: Hurwitz.one
lemma Hurwitz.one_re line 124 source
no axioms what this means
Statement uses: Eq, Int, Hurwitz.re, OfNat.ofNat, Hurwitz
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
lemma Hurwitz.one_im_o line 125 source
no axioms what this means
Statement uses: Eq, Int, Hurwitz.imO, OfNat.ofNat, Hurwitz
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
lemma Hurwitz.one_im_i line 126 source
no axioms what this means
Statement uses: Eq, Int, Hurwitz.imI, OfNat.ofNat, Hurwitz
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
lemma Hurwitz.one_im_oi line 127 source
no axioms what this means
Statement uses: Eq, Int, Hurwitz.imOI, OfNat.ofNat, Hurwitz
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
lemma Hurwitz.toQuaternion_one line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Quaternion, Real, Hurwitz.toQuaternion, OfNat.ofNat, Hurwitz, Neg.neg
Proof uses: Quaternion.ext, of_eq_true, QuaternionAlgebra.re, Eq.trans, True, congrFun', congrArg, QuaternionAlgebra.mk, congr, QuaternionAlgebra, HSub.hSub, Hurwitz.re, HMul.hMul, Inv.inv, Hurwitz.imO, Hurwitz.imOI, HAdd.hAdd, Hurwitz.imI, Int.cast_one, Int.cast_zero and 8 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Hurwitz.neg The negation -z of a Hurwitz number line 137 source
Source documentation
The negation -z of a Hurwitz number

no axioms what this means
Statement uses: Hurwitz
Proof uses: Hurwitz.mk, Neg.neg, Int, Hurwitz.re, Hurwitz.imO, Hurwitz.imI, Hurwitz.imOI
1 instances, coercions and auxiliary constants left out.
```
def neg (z : 𝓞) : 𝓞 := ⟨-re z, -imO z, -imI z, -imOI z⟩
```
instance Hurwitz.(instance at line 140) line 140 source
Source documentation
Notation - for negation
```
instance : Neg 𝓞 := ⟨neg⟩
```
Mentions: Hurwitz.neg
lemma Hurwitz.neg_re how neg interacts with re and im_* line 143 source
Source comment
how neg interacts with re and im_*

no axioms what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.re, Neg.neg
Proof uses: rfl
3 instances, coercions and auxiliary constants left out.
```
@[simp] lemma neg_re (z : 𝓞) : re (-z) = -re z  := rfl
```
lemma Hurwitz.neg_im_o how neg interacts with re and im_* line 144 source
Source comment
how neg interacts with re and im_*

no axioms what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.imO, Neg.neg
Proof uses: rfl
3 instances, coercions and auxiliary constants left out.
```
@[simp] lemma neg_im_o (z : 𝓞) : imO (-z) = -imO z  := rfl
```
lemma Hurwitz.neg_im_i how neg interacts with re and im_* line 145 source
Source comment
how neg interacts with re and im_*

no axioms what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.imI, Neg.neg
Proof uses: rfl
3 instances, coercions and auxiliary constants left out.
```
@[simp] lemma neg_im_i (z : 𝓞) : imI (-z) = -imI z  := rfl
```
lemma Hurwitz.neg_im_oi how neg interacts with re and im_* line 146 source
Source comment
how neg interacts with re and im_*

no axioms what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.imOI, Neg.neg
Proof uses: rfl
3 instances, coercions and auxiliary constants left out.
```
@[simp] lemma neg_im_oi (z : 𝓞) : imOI (-z) = -imOI z  := rfl
…
```
lemma Hurwitz.toQuaternion_neg line 149 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Eq, Quaternion, Real, Hurwitz.toQuaternion, Neg.neg, OfNat.ofNat
Proof uses: Quaternion.ext, Eq.mpr, QuaternionAlgebra.re, HAdd.hAdd, Hurwitz.re, HMul.hMul, Inv.inv, Hurwitz.imO, Hurwitz.imOI, HSub.hSub, id, congr, congrArg, QuaternionAlgebra.mk, Hurwitz.imI, QuaternionAlgebra, Eq.trans, Int.cast_neg, mul_neg, sub_neg_eq_add and 60 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Hurwitz.add addition z+w of complex numbers line 158 source
Source documentation
addition z+w of complex numbers

no axioms what this means
Statement uses: Hurwitz
Proof uses: Hurwitz.mk, HAdd.hAdd, Int, Hurwitz.re, Hurwitz.imO, Hurwitz.imI, Hurwitz.imOI
2 instances, coercions and auxiliary constants left out.
```
def add (z w : 𝓞) : 𝓞 := ⟨z.re + w.re, z.imO + w.imO, z.imI + w.imI, z.imOI + w.imOI⟩
```
instance Hurwitz.(instance at line 161) line 161 source
Source documentation
Notation + for addition
```
instance : Add 𝓞 := ⟨add⟩
```
Mentions: Hurwitz.add
lemma Hurwitz.add_re basic properties line 164 source
Source comment
basic properties

no axioms what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.re, HAdd.hAdd
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
```
@[simp] lemma add_re (z w : 𝓞) : re (z + w) = re z  + re w  := rfl
```
lemma Hurwitz.add_im_o basic properties line 165 source
Source comment
basic properties

no axioms what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.imO, HAdd.hAdd
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
```
@[simp] lemma add_im_o (z w : 𝓞) : imO (z + w) = imO z  + imO w  := rfl
```
lemma Hurwitz.add_im_i basic properties line 166 source
Source comment
basic properties

no axioms what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.imI, HAdd.hAdd
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
```
@[simp] lemma add_im_i (z w : 𝓞) : imI (z + w) = imI z  + imI w  := rfl
```
lemma Hurwitz.add_im_oi basic properties line 167 source
Source comment
basic properties

no axioms what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.imOI, HAdd.hAdd
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
```
@[simp] lemma add_im_oi (z w : 𝓞) : imOI (z + w) = imOI z  + imOI w  := rfl
…
```
lemma Hurwitz.toQuaternion_add line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Eq, Quaternion, Real, Hurwitz.toQuaternion, HAdd.hAdd, Neg.neg, OfNat.ofNat
Proof uses: Quaternion.ext, Eq.mpr, QuaternionAlgebra.re, HSub.hSub, Hurwitz.re, HMul.hMul, Inv.inv, Hurwitz.imO, Hurwitz.imOI, id, congrFun', congrArg, QuaternionAlgebra.mk, Hurwitz.imI, congr, QuaternionAlgebra, Int.cast_add, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat and 47 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance Hurwitz.(instance at line 175) line 175 source
Source documentation
Notation + for addition
```
instance : Sub 𝓞 := ⟨fun a b => a + -b⟩
```
lemma Hurwitz.toQuaternion_sub line 177 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Eq, Quaternion, Real, Hurwitz.toQuaternion, HSub.hSub, Neg.neg, OfNat.ofNat
Proof uses: Eq.mpr, HAdd.hAdd, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, id, congrArg, sub_eq_add_neg, Hurwitz.toQuaternion_neg, Hurwitz.toQuaternion_add
37 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance Hurwitz.(instance at line 192) line 192 source
lemma Hurwitz.preserves_nsmulRec line 195 source
standard axioms: propext what this means
Statement uses: Zero, Add, AddMonoid, Eq, OfNat.ofNat, HAdd.hAdd, Nat, nsmulRec, HSMul.hSMul
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, nsmulRec.eq_1, zero_smul, Eq.refl, Nat.succ, nsmulRec.eq_2, add_nsmul, one_nsmul
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.toQuaternion_nsmul line 202 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Nat, Eq, Quaternion, Real, Hurwitz.toQuaternion, HSMul.hSMul, Neg.neg, OfNat.ofNat
Proof uses: Hurwitz.preserves_nsmulRec, Hurwitz.toQuaternion_zero, Hurwitz.toQuaternion_add
26 instances, coercions and auxiliary constants left out.
instance Hurwitz.(instance at line 206) line 206 source
lemma Hurwitz.preserves_zsmul line 209 source
no axioms what this means
Statement uses: Zero, Add, Neg, SMul, Nat, SubNegMonoid, Eq, HSMul.hSMul, Neg.neg, Int, zsmulRec
Proof uses: Int.ofNat, Eq.mpr, id, congrArg, zsmulRec.eq_1, Int.ofNat_eq_natCast, natCast_zsmul, Eq.refl, Eq.symm, Int.negSucc, Nat.succ, zsmulRec.eq_2, HAdd.hAdd, OfNat.ofNat, negSucc_zsmul
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.toQuaternion_zsmul line 220 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Int, Eq, Quaternion, Real, Hurwitz.toQuaternion, HSMul.hSMul, Neg.neg, OfNat.ofNat
Proof uses: Hurwitz.preserves_zsmul, Hurwitz.toQuaternion_nsmul, Hurwitz.toQuaternion_neg
28 instances, coercions and auxiliary constants left out.
def Hurwitz.mul Multiplication z*w of two Hurwitz numbers line 242 source
Source documentation
Multiplication z*w of two Hurwitz numbers

no axioms what this means
Statement uses: Hurwitz
Proof uses: Hurwitz.mk, HSub.hSub, Int, HAdd.hAdd, HMul.hMul, Hurwitz.re, Hurwitz.imO, Hurwitz.imI, Hurwitz.imOI
6 instances, coercions and auxiliary constants left out.
```
def mul (z w : 𝓞) : 𝓞 where
…
```
instance Hurwitz.(instance at line 253) line 253 source
Source documentation
Notation * for multiplication
```
instance : Mul 𝓞 := ⟨mul⟩
```
Mentions: Hurwitz.mul
lemma Hurwitz.mul_re how mul reacts with re and im line 256 source
Source comment
how `mul` reacts with `re` and `im`

no axioms what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.re, HMul.hMul, HSub.hSub, HAdd.hAdd, Hurwitz.imO, Hurwitz.imI, Hurwitz.imOI
Proof uses: rfl
9 instances, coercions and auxiliary constants left out.
```
@[simp] lemma mul_re (z w : 𝓞) :
    re (z * w) = z.re * w.re - z.imO * w.imO - z.imI * w.imO -
      z.imI * w.imI + z.imI * w.imOI - z.imOI * w.imOI := rfl
```
lemma Hurwitz.mul_im_o line 260 source
no axioms what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.imO, HMul.hMul, HAdd.hAdd, HSub.hSub, Hurwitz.re, Hurwitz.imOI, Hurwitz.imI
Proof uses: rfl
9 instances, coercions and auxiliary constants left out.
lemma Hurwitz.mul_im_i line 264 source
no axioms what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.imI, HMul.hMul, HSub.hSub, HAdd.hAdd, Hurwitz.re, Hurwitz.imO, Hurwitz.imOI
Proof uses: rfl
9 instances, coercions and auxiliary constants left out.
lemma Hurwitz.mul_im_oi line 268 source
no axioms what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.imOI, HMul.hMul, HSub.hSub, HAdd.hAdd, Hurwitz.re, Hurwitz.imI, Hurwitz.imO
Proof uses: rfl
9 instances, coercions and auxiliary constants left out.
lemma Hurwitz.toQuaternion_mul line 273 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Eq, Quaternion, Real, Hurwitz.toQuaternion, HMul.hMul, Neg.neg, OfNat.ofNat
Proof uses: Quaternion.ext, Eq.mpr, QuaternionAlgebra.re, HSub.hSub, HAdd.hAdd, Hurwitz.re, Hurwitz.imO, Hurwitz.imI, Hurwitz.imOI, Inv.inv, id, congr, congrArg, QuaternionAlgebra.mk, QuaternionAlgebra, Eq.trans, Int, Int.cast_sub, Int.cast_add, Int.cast_mul and 84 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.o_mul_i line 277 source
standard axioms: propext what this means
Statement uses: Eq, Hurwitz, HMul.hMul, Hurwitz.mk, OfNat.ofNat, Int
Proof uses: Hurwitz.ext, of_eq_true, Hurwitz.re, Eq.trans, True, congrFun', congrArg, HSub.hSub, HAdd.hAdd, Hurwitz.imO, Hurwitz.imI, Hurwitz.imOI, congr, MulZeroClass.mul_zero, sub_self, mul_one, add_zero, eq_self, zero_add, sub_zero
28 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance Hurwitz.(instance at line 282) line 282 source
lemma Hurwitz.preserves_npowRec line 284 source
no axioms what this means
Statement uses: One, Mul, Monoid, Eq, OfNat.ofNat, HMul.hMul, Nat, npowRec, HPow.hPow
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, npowRec.eq_1, pow_zero, Eq.refl, HAdd.hAdd, Nat.succ, npowRec.eq_2, pow_succ
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.toQuaternion_npow line 291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Nat, Eq, Quaternion, Real, Hurwitz.toQuaternion, HPow.hPow, Neg.neg, OfNat.ofNat
Proof uses: Hurwitz.preserves_npowRec, Hurwitz.toQuaternion_one, Hurwitz.toQuaternion_mul
24 instances, coercions and auxiliary constants left out.
instance Hurwitz.(instance at line 294) line 294 source
lemma Hurwitz.preserves_unaryCast line 296 source
standard axioms: propext what this means
Statement uses: One, Zero, Add, AddMonoidWithOne, Eq, OfNat.ofNat, HAdd.hAdd, Nat, Nat.unaryCast
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, Nat.unaryCast.eq_1, Nat.cast_zero, Eq.refl, Nat.succ, Nat.unaryCast.eq_2, Nat.cast_add, Nat.cast_one
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.toQuaternion_natCast line 304 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Quaternion, Real, Hurwitz.toQuaternion, Hurwitz, Neg.neg, OfNat.ofNat
Proof uses: Hurwitz.preserves_unaryCast, Hurwitz.toQuaternion_zero, Hurwitz.toQuaternion_one, Hurwitz.toQuaternion_add
24 instances, coercions and auxiliary constants left out.
instance Hurwitz.(instance at line 307) line 307 source
lemma Hurwitz.Int.castDef_ofNat line 309 source
no axioms what this means
Statement uses: NatCast, Neg, Nat, Eq, Int.castDef, Int.ofNat
Proof uses: rfl
1 instances, coercions and auxiliary constants left out.
lemma Hurwitz.Int.castDef_negSucc line 312 source
no axioms what this means
Statement uses: NatCast, Neg, Nat, Eq, Int.castDef, Int.negSucc, Neg.neg, HAdd.hAdd, OfNat.ofNat
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
lemma Hurwitz.preserves_castDef line 315 source
standard axioms: propext what this means
Statement uses: NatCast, Neg, AddGroupWithOne, Nat, Eq, Neg.neg, Int, Int.castDef
Proof uses: Int.ofNat, Eq.mpr, id, congrArg, Hurwitz.Int.castDef_ofNat, Int.ofNat_eq_natCast, Int.cast_natCast, Eq.refl, Eq.symm, Int.negSucc, HAdd.hAdd, OfNat.ofNat, Hurwitz.Int.castDef_negSucc, Int.cast_negSucc
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.toQuaternion_intCast line 323 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, Quaternion, Real, Hurwitz.toQuaternion, Hurwitz, Neg.neg, OfNat.ofNat
Proof uses: Hurwitz.preserves_castDef, Hurwitz.toQuaternion_natCast, Hurwitz.toQuaternion_neg
21 instances, coercions and auxiliary constants left out.
instance Hurwitz.ring line 326 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Hurwitz
Proof uses: Function.Injective.ring, Quaternion, Real, Hurwitz.toQuaternion, Hurwitz.toQuaternion_injective, Neg.neg, OfNat.ofNat, Hurwitz.toQuaternion_zero, Hurwitz.toQuaternion_one, Hurwitz.toQuaternion_add, Hurwitz.toQuaternion_mul, Hurwitz.toQuaternion_neg, Hurwitz.toQuaternion_sub, Nat, Hurwitz.toQuaternion_nsmul, Int, Hurwitz.toQuaternion_zsmul, Hurwitz.toQuaternion_npow, Hurwitz.toQuaternion_natCast, Hurwitz.toQuaternion_intCast
18 instances, coercions and auxiliary constants left out.
lemma Hurwitz.natCast_re line 341 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Hurwitz.re, Hurwitz
Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congr, congrArg, Nat.cast_zero, CharP.cast_eq_zero, eq_self, Eq.mpr, HAdd.hAdd, id, Nat.cast_add, Nat.cast_one
45 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.natCast_im_o line 345 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Hurwitz.imO, Hurwitz, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, Nat.cast_zero, eq_self, Eq.mpr, HAdd.hAdd, id, Nat.cast_add, Nat.cast_one, add_zero
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.natCast_im_i line 349 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Hurwitz.imI, Hurwitz, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, Nat.cast_zero, eq_self, Eq.mpr, HAdd.hAdd, id, Nat.cast_add, Nat.cast_one, add_zero
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.natCast_im_oi line 353 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Hurwitz.imOI, Hurwitz, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, Nat.cast_zero, eq_self, Eq.mpr, HAdd.hAdd, id, Nat.cast_add, Nat.cast_one, add_zero
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.intCast_re line 358 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, Hurwitz.re, Hurwitz
Proof uses: Nat, Int.ofNat, of_eq_true, Eq.trans, True, congrFun', congrArg, Int.cast_natCast, Hurwitz.natCast_re, eq_self, Eq.symm, Int.negSucc, HAdd.hAdd, Neg.neg, OfNat.ofNat, congr, Nat.succ, Nat.cast_add, Nat.cast_one, neg_add_rev and 4 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.intCast_im_o line 362 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, Hurwitz.imO, Hurwitz, OfNat.ofNat
Proof uses: Nat, Int.ofNat, of_eq_true, Eq.trans, True, congrFun', congrArg, Int.cast_natCast, Hurwitz.natCast_im_o, eq_self, Eq.symm, Int.negSucc, HAdd.hAdd, Neg.neg, Nat.succ, Nat.cast_add, Nat.cast_one, neg_add_rev, Int.cast_add, congr and 5 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.intCast_im_i line 366 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, Hurwitz.imI, Hurwitz, OfNat.ofNat
Proof uses: Nat, Int.ofNat, of_eq_true, Eq.trans, True, congrFun', congrArg, Int.cast_natCast, Hurwitz.natCast_im_i, eq_self, Eq.symm, Int.negSucc, HAdd.hAdd, Neg.neg, Nat.succ, Nat.cast_add, Nat.cast_one, neg_add_rev, Int.cast_add, congr and 5 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.intCast_im_oi line 370 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, Hurwitz.imOI, Hurwitz, OfNat.ofNat
Proof uses: Nat, Int.ofNat, of_eq_true, Eq.trans, True, congrFun', congrArg, Int.cast_natCast, Hurwitz.natCast_im_oi, eq_self, Eq.symm, Int.negSucc, HAdd.hAdd, Neg.neg, Nat.succ, Nat.cast_add, Nat.cast_one, neg_add_rev, Int.cast_add, congr and 5 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance Hurwitz.starRing Conjugate; sends $a+bi+cj+dk$ to $a-bi-cj-dk$ line 377 source
Source documentation
Conjugate; sends $a+bi+cj+dk$ to $a-bi-cj-dk$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: StarRing, Hurwitz
Proof uses: StarRing.mk, StarMul.mk, InvolutiveStar.mk, Star.mk, Hurwitz.mk, HSub.hSub, Int, Hurwitz.re, Hurwitz.imO, Hurwitz.imOI, Neg.neg, Hurwitz.imI
16 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
instance starRing : StarRing 𝓞 where
…
```
lemma Hurwitz.star_re line 383 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.re, Star.star, HSub.hSub, Hurwitz.imO, Hurwitz.imOI
Proof uses: rfl
22 instances, coercions and auxiliary constants left out.
lemma Hurwitz.star_im_o line 384 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.imO, Star.star, Neg.neg
Proof uses: rfl
21 instances, coercions and auxiliary constants left out.
lemma Hurwitz.star_im_i line 385 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.imI, Star.star, Neg.neg
Proof uses: rfl
21 instances, coercions and auxiliary constants left out.
lemma Hurwitz.star_im_oi line 386 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.imOI, Star.star, Neg.neg
Proof uses: rfl
21 instances, coercions and auxiliary constants left out.
lemma Hurwitz.toQuaternion_star line 389 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Eq, Quaternion, Real, Hurwitz.toQuaternion, Star.star, Neg.neg, OfNat.ofNat
Proof uses: Quaternion.ext, Eq.mpr, QuaternionAlgebra.re, HSub.hSub, Int, Hurwitz.re, Hurwitz.imO, Hurwitz.imOI, HMul.hMul, Inv.inv, id, congrArg, Quaternion.re_star, QuaternionAlgebra.mk, HAdd.hAdd, Hurwitz.imI, inferInstance, CommGroupWithZero, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval and 87 more
132 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.star_eq line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Eq, Star.star, Function.comp, Quaternion, Real, Hurwitz.fromQuaternion, Neg.neg, OfNat.ofNat, Hurwitz.toQuaternion
Proof uses: Eq.mpr, id, congrArg, Hurwitz.leftInverse_fromQuaternion_toQuaternion, Eq.refl
35 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance Hurwitz.(instance at line 401) line 401 source
def Hurwitz.norm The norm of a Hurwitz integer: the integer z * star z, equivalently the squared absolute value of the corresponding quaternion line 406 source
Source documentation
The norm of a Hurwitz integer: the integer z * star z, equivalently the squared absolute value of the corresponding quaternion.

no axioms what this means
Statement uses: Hurwitz, Int
Proof uses: HAdd.hAdd, HSub.hSub, HMul.hMul, Hurwitz.re, Hurwitz.imO, Hurwitz.imI, Hurwitz.imOI
6 instances, coercions and auxiliary constants left out.
```
def norm (z : 𝓞) : ℤ :=
…
```
lemma Hurwitz.norm_eq_mul_conj line 410 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Eq, Hurwitz.norm, HMul.hMul, Star.star
Proof uses: Hurwitz.ext, Eq.mpr, Int, Hurwitz.re, HAdd.hAdd, HSub.hSub, Hurwitz.imO, Hurwitz.imI, Hurwitz.imOI, Neg.neg, id, congrFun', congrArg, Hurwitz.intCast_re, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance and 46 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.coe_norm line 414 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Eq, Real, Hurwitz.norm, HAdd.hAdd, HPow.hPow, Nat, HSub.hSub, Hurwitz.re, HMul.hMul, Inv.inv, OfNat.ofNat, Hurwitz.imO, Hurwitz.imOI, Hurwitz.imI
Proof uses: Eq.mpr, Int, id, congrArg, Hurwitz.norm.eq_1, inferInstance, CommGroupWithZero, GroupWithZero, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Neg.neg, List.nil, Prod, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, rfl, Eq.trans, Eq.refl, Mathlib.Tactic.FieldSimp.NF.atom_eq_eval and 94 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.norm_zero line 425 source
standard axioms: propext what this means
Statement uses: Eq, Int, Hurwitz.norm, OfNat.ofNat, Hurwitz
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HAdd.hAdd, HSub.hSub, HMul.hMul, Hurwitz.re, Hurwitz.imO, Hurwitz.imI, Hurwitz.imOI, congr, MulZeroClass.mul_zero, add_zero, sub_self, eq_self
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.norm_one line 427 source
standard axioms: propext what this means
Statement uses: Eq, Int, Hurwitz.norm, OfNat.ofNat, Hurwitz
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HAdd.hAdd, HSub.hSub, HMul.hMul, Hurwitz.re, Hurwitz.imO, Hurwitz.imI, Hurwitz.imOI, congr, mul_one, MulZeroClass.mul_zero, add_zero, sub_zero, sub_self, eq_self
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.norm_mul line 429 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Eq, Int, Hurwitz.norm, HMul.hMul
Proof uses: Eq.mpr, id, congrArg, Eq.symm, propext, Int.cast_inj, Star.star, congrFun', Hurwitz.norm_eq_mul_conj, StarMul.star_mul, mul_assoc, Int.cast_comm, Int.cast_mul, Eq.refl
32 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.norm_nonneg line 435 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, LE.le, Int, OfNat.ofNat, Hurwitz.norm
Proof uses: Eq.mpr, Real, id, Eq, congrArg, Eq.symm, propext, Int.cast_nonneg_iff, HAdd.hAdd, HPow.hPow, Nat, HSub.hSub, Hurwitz.re, HMul.hMul, Inv.inv, Hurwitz.imO, Hurwitz.imOI, Hurwitz.imI, Hurwitz.coe_norm, add_nonneg and 2 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.norm_eq_zero line 439 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Iff, Eq, Int, Hurwitz.norm, OfNat.ofNat
Proof uses: Iff.intro, HPow.hPow, Nat, HSub.hSub, Hurwitz.imO, Hurwitz.imOI, eq_zero_of_add_nonpos_right, HAdd.hAdd, HMul.hMul, Hurwitz.re, Hurwitz.imI, add_nonneg, Even.pow_nonneg, even_two_mul, Eq.le, Eq.mp, Real, inferInstance, GroupWithZero, CommGroupWithZero and 76 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.normSq_toQuaternion line 464 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Eq, Real, MonoidWithZeroHom, Quaternion, Neg.neg, OfNat.ofNat, Quaternion.normSq, Hurwitz.toQuaternion, Hurwitz.norm
Proof uses: Quaternion.coe_injective, Eq.mpr, HMul.hMul, Star.star, id, congrArg, Eq.symm, Quaternion.self_mul_star, Hurwitz.toQuaternion_star, Hurwitz.toQuaternion_mul, Hurwitz.norm_eq_mul_conj, Hurwitz.toQuaternion_intCast, Quaternion.coe_intCast, Eq.refl
69 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.aux line 470 source
lemma Hurwitz.aux2 line 476 source
lemma Hurwitz.exists_near line 495 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Quaternion, Real, Exists, Hurwitz, LT.lt, Dist.dist, Hurwitz.toQuaternion, OfNat.ofNat
Proof uses: Eq, Inv.inv, Nat, HPow.hPow, Mathlib.Meta.NormNum.isNNRat_eq_true, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNNRat_pow, Mathlib.Meta.NormNum.one_natPow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit0, LE.le, HSub.hSub, round, Eq.mpr, id, congrArg and 92 more
179 instances, coercions and auxiliary constants left out.

Tactic trace: 59 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.quot_rem line 541 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hurwitz, Ne, OfNat.ofNat, Exists, And, Eq, HAdd.hAdd, HMul.hMul, LT.lt, Int, Hurwitz.norm
Proof uses: Quaternion, Real, Hurwitz.toQuaternion, Neg.neg, Iff.mpr, Hurwitz.toQuaternion_ne_zero_iff, HDiv.hDiv, Dist.dist, Hurwitz.exists_near, Exists.intro, HSub.hSub, And.intro, Eq.symm, add_sub_cancel, Eq.mpr, id, congrArg, propext, Int.cast_lt, MonoidWithZeroHom and 18 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma Hurwitz.left_ideal_princ line 565 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Submodule, Hurwitz, Exists, Eq, Submodule.span, Singleton.singleton, Set
Proof uses: dite, Bot.bot, Exists.intro, OfNat.ofNat, Eq.mpr, id, congrArg, propext, Eq.comm, of_eq_true, Eq.trans, True, eq_self, Not, Subtype, And, Membership.mem, Ne, Nonempty, Submodule.exists_mem_ne_zero_of_ne_bot and 38 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.