Hurwitz

Statistics

Metric	Count
Definitions `Hurwitz`, `add`, `fromQuaternion`, `im_i`, `im_o`, `im_oi`, `instAdd`, `instIntCast`, `instMul`, `instNatCast`, `instNeg`, `instOne`, `instPowNat`, `instSMulInt`, `instSMulNat`, `instSub`, `instZero`, `mul`, `neg`, `norm`, `one`, `re`, `ring`, `starRing`, `toQuaternion`, `zero`, `term𝓞`	27
Theorems `castDef_negSucc`, `castDef_ofNat`, `add_im_i`, `add_im_o`, `add_im_oi`, `add_re`, `coe_norm`, `exists_near`, `ext`, `ext_iff`, `fromQuaternion_injOn`, `instCharZero`, `intCast_im_i`, `intCast_im_o`, `intCast_im_oi`, `intCast_re`, `leftInvOn_toQuaternion_fromQuaternion`, `leftInverse_fromQuaternion_toQuaternion`, `left_ideal_princ`, `mul_im_i`, `mul_im_o`, `mul_im_oi`, `mul_re`, `natCast_im_i`, `natCast_im_o`, `natCast_im_oi`, `natCast_re`, `neg_im_i`, `neg_im_o`, `neg_im_oi`, `neg_re`, `normSq_toQuaternion`, `norm_eq_mul_conj`, `norm_eq_zero`, `norm_mul`, `norm_nonneg`, `norm_one`, `norm_zero`, `o_mul_i`, `one_im_i`, `one_im_o`, `one_im_oi`, `one_re`, `preserves_castDef`, `preserves_npowRec`, `preserves_nsmulRec`, `preserves_unaryCast`, `preserves_zsmul`, `quot_rem`, `star_eq`, `star_im_i`, `star_im_o`, `star_im_oi`, `star_re`, `toQuaternion_add`, `toQuaternion_eq_zero_iff`, `toQuaternion_injective`, `toQuaternion_intCast`, `toQuaternion_mul`, `toQuaternion_natCast`, `toQuaternion_ne_zero_iff`, `toQuaternion_neg`, `toQuaternion_npow`, `toQuaternion_nsmul`, `toQuaternion_one`, `toQuaternion_star`, `toQuaternion_sub`, `toQuaternion_zero`, `toQuaternion_zsmul`, `zero_im_i`, `zero_im_o`, `zero_im_oi`, `zero_re`	73
Total	100

Hurwitz

Definitions

Name	Category	Theorems
`add` 📖	CompOp	—
`fromQuaternion` 📖	CompOp	4 math math: `leftInverse_fromQuaternion_toQuaternion`, `leftInvOn_toQuaternion_fromQuaternion`, `fromQuaternion_injOn`, `star_eq`
`im_i` 📖	CompOp	13 math math: `mul_re`, `star_im_i`, `mul_im_oi`, `natCast_im_i`, `mul_im_i`, `coe_norm`, `zero_im_i`, `intCast_im_i`, `mul_im_o`, `add_im_i`, `ext_iff`, `neg_im_i`, `one_im_i`
`im_o` 📖	CompOp	14 math math: `neg_im_o`, `mul_re`, `mul_im_oi`, `mul_im_i`, `zero_im_o`, `star_im_o`, `one_im_o`, `coe_norm`, `star_re`, `intCast_im_o`, `mul_im_o`, `natCast_im_o`, `add_im_o`, `ext_iff`
`im_oi` 📖	CompOp	14 math math: `mul_re`, `mul_im_oi`, `mul_im_i`, `star_im_oi`, `neg_im_oi`, `intCast_im_oi`, `add_im_oi`, `coe_norm`, `star_re`, `zero_im_oi`, `mul_im_o`, `natCast_im_oi`, `one_im_oi`, `ext_iff`
`instAdd` 📖	CompOp	6 math math: `add_im_oi`, `add_re`, `toQuaternion_add`, `add_im_i`, `add_im_o`, `quot_rem`
`instIntCast` 📖	CompOp	6 math math: `intCast_im_oi`, `toQuaternion_intCast`, `intCast_im_o`, `intCast_im_i`, `norm_eq_mul_conj`, `intCast_re`
`instMul` 📖	CompOp	9 math math: `mul_re`, `o_mul_i`, `mul_im_oi`, `mul_im_i`, `toQuaternion_mul`, `mul_im_o`, `norm_eq_mul_conj`, `norm_mul`, `quot_rem`
`instNatCast` 📖	CompOp	5 math math: `natCast_re`, `natCast_im_i`, `natCast_im_oi`, `natCast_im_o`, `toQuaternion_natCast`
`instNeg` 📖	CompOp	5 math math: `neg_im_o`, `neg_im_oi`, `neg_re`, `toQuaternion_neg`, `neg_im_i`
`instOne` 📖	CompOp	7 math math: `HurwitzRatHat.canonicalForm`, `one_im_o`, `toQuaternion_one`, `one_im_oi`, `one_re`, `norm_one`, `one_im_i`
`instPowNat` 📖	CompOp	1 math math: `toQuaternion_npow`
`instSMulInt` 📖	CompOp	1 math math: `toQuaternion_zsmul`
`instSMulNat` 📖	CompOp	1 math math: `toQuaternion_nsmul`
`instSub` 📖	CompOp	1 math math: `toQuaternion_sub`
`instZero` 📖	CompOp	8 math math: `toQuaternion_zero`, `norm_zero`, `zero_im_o`, `zero_im_i`, `zero_im_oi`, `norm_eq_zero`, `toQuaternion_eq_zero_iff`, `zero_re`
`mul` 📖	CompOp	—
`neg` 📖	CompOp	—
`norm` 📖	CompOp	9 math math: `norm_zero`, `coe_norm`, `normSq_toQuaternion`, `norm_eq_mul_conj`, `norm_eq_zero`, `norm_nonneg`, `norm_one`, `norm_mul`, `quot_rem`
`one` 📖	CompOp	—
`re` 📖	CompOp	13 math math: `natCast_re`, `mul_re`, `mul_im_oi`, `mul_im_i`, `neg_re`, `add_re`, `coe_norm`, `star_re`, `mul_im_o`, `one_re`, `ext_iff`, `zero_re`, `intCast_re`
`ring` 📖	CompOp	10 math math: `star_im_i`, `toQuaternion_star`, `left_ideal_princ`, `star_im_oi`, `HurwitzRatHat.canonicalForm`, `star_im_o`, `star_re`, `norm_eq_mul_conj`, `instCharZero`, `star_eq`
`starRing` 📖	CompOp	7 math math: `star_im_i`, `toQuaternion_star`, `star_im_oi`, `star_im_o`, `star_re`, `norm_eq_mul_conj`, `star_eq`
`toQuaternion` 📖	CompOp	19 math math: `exists_near`, `toQuaternion_sub`, `toQuaternion_zero`, `toQuaternion_zsmul`, `toQuaternion_star`, `leftInverse_fromQuaternion_toQuaternion`, `toQuaternion_mul`, `toQuaternion_nsmul`, `toQuaternion_npow`, `toQuaternion_intCast`, `toQuaternion_add`, `normSq_toQuaternion`, `toQuaternion_neg`, `toQuaternion_one`, `leftInvOn_toQuaternion_fromQuaternion`, `star_eq`, `toQuaternion_injective`, `toQuaternion_eq_zero_iff`, `toQuaternion_natCast`
`zero` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_im_i` 📖	mathematical	—	`im_i` `Hurwitz` `instAdd`	—	—
`add_im_o` 📖	mathematical	—	`im_o` `Hurwitz` `instAdd`	—	—
`add_im_oi` 📖	mathematical	—	`im_oi` `Hurwitz` `instAdd`	—	—
`add_re` 📖	mathematical	—	`re` `Hurwitz` `instAdd`	—	—
`coe_norm` 📖	mathematical	—	`norm` `re` `im_o` `im_oi` `im_i`	—	`norm.eq_1`
`exists_near` 📖	mathematical	—	`toQuaternion`	—	`leftInvOn_toQuaternion_fromQuaternion`
`ext` 📖	—	`re` `im_o` `im_i` `im_oi`	—	—	—
`ext_iff` 📖	mathematical	—	`re` `im_o` `im_i` `im_oi`	—	`ext`
`fromQuaternion_injOn` 📖	mathematical	—	`Hurwitz` `fromQuaternion`	—	`leftInvOn_toQuaternion_fromQuaternion`
`instCharZero` 📖	mathematical	—	`Hurwitz` `ring`	—	`natCast_re` `natCast_im_o` `natCast_im_i` `natCast_im_oi`
`intCast_im_i` 📖	mathematical	—	`im_i` `Hurwitz` `instIntCast`	—	`natCast_im_i`
`intCast_im_o` 📖	mathematical	—	`im_o` `Hurwitz` `instIntCast`	—	`natCast_im_o`
`intCast_im_oi` 📖	mathematical	—	`im_oi` `Hurwitz` `instIntCast`	—	`natCast_im_oi`
`intCast_re` 📖	mathematical	—	`re` `Hurwitz` `instIntCast`	—	`natCast_re`
`leftInvOn_toQuaternion_fromQuaternion` 📖	mathematical	—	`Hurwitz` `toQuaternion` `fromQuaternion`	—	—
`leftInverse_fromQuaternion_toQuaternion` 📖	mathematical	—	`Hurwitz` `fromQuaternion` `toQuaternion`	—	—
`left_ideal_princ` 📖	mathematical	—	`Hurwitz` `ring`	—	`norm_nonneg` `quot_rem`
`mul_im_i` 📖	mathematical	—	`im_i` `Hurwitz` `instMul` `re` `im_o` `im_oi`	—	—
`mul_im_o` 📖	mathematical	—	`im_o` `Hurwitz` `instMul` `re` `im_oi` `im_i`	—	—
`mul_im_oi` 📖	mathematical	—	`im_oi` `Hurwitz` `instMul` `re` `im_i` `im_o`	—	—
`mul_re` 📖	mathematical	—	`re` `Hurwitz` `instMul` `im_o` `im_i` `im_oi`	—	—
`natCast_im_i` 📖	mathematical	—	`im_i` `Hurwitz` `instNatCast`	—	—
`natCast_im_o` 📖	mathematical	—	`im_o` `Hurwitz` `instNatCast`	—	—
`natCast_im_oi` 📖	mathematical	—	`im_oi` `Hurwitz` `instNatCast`	—	—
`natCast_re` 📖	mathematical	—	`re` `Hurwitz` `instNatCast`	—	—
`neg_im_i` 📖	mathematical	—	`im_i` `Hurwitz` `instNeg`	—	—
`neg_im_o` 📖	mathematical	—	`im_o` `Hurwitz` `instNeg`	—	—
`neg_im_oi` 📖	mathematical	—	`im_oi` `Hurwitz` `instNeg`	—	—
`neg_re` 📖	mathematical	—	`re` `Hurwitz` `instNeg`	—	—
`normSq_toQuaternion` 📖	mathematical	—	`toQuaternion` `norm`	—	`toQuaternion_star` `toQuaternion_mul` `norm_eq_mul_conj` `toQuaternion_intCast`
`norm_eq_mul_conj` 📖	mathematical	—	`Hurwitz` `instIntCast` `norm` `instMul` `ring` `starRing`	—	`ext` `intCast_re` `intCast_im_o` `intCast_im_i` `intCast_im_oi`
`norm_eq_zero` 📖	mathematical	—	`norm` `Hurwitz` `instZero`	—	`coe_norm` `ext` `norm_zero`
`norm_mul` 📖	mathematical	—	`norm` `Hurwitz` `instMul`	—	`instCharZero` `norm_eq_mul_conj`
`norm_nonneg` 📖	mathematical	—	`norm`	—	`coe_norm`
`norm_one` 📖	mathematical	—	`norm` `Hurwitz` `instOne`	—	—
`norm_zero` 📖	mathematical	—	`norm` `Hurwitz` `instZero`	—	—
`o_mul_i` 📖	mathematical	—	`Hurwitz` `instMul`	—	`ext`
`one_im_i` 📖	mathematical	—	`im_i` `Hurwitz` `instOne`	—	—
`one_im_o` 📖	mathematical	—	`im_o` `Hurwitz` `instOne`	—	—
`one_im_oi` 📖	mathematical	—	`im_oi` `Hurwitz` `instOne`	—	—
`one_re` 📖	mathematical	—	`re` `Hurwitz` `instOne`	—	—
`preserves_castDef` 📖	—	—	—	—	`Int.castDef_ofNat` `Int.castDef_negSucc`
`preserves_npowRec` 📖	—	—	—	—	—
`preserves_nsmulRec` 📖	—	—	—	—	—
`preserves_unaryCast` 📖	—	—	—	—	—
`preserves_zsmul` 📖	—	—	—	—	—
`quot_rem` 📖	mathematical	—	`Hurwitz` `instAdd` `instMul` `norm`	—	`toQuaternion_ne_zero_iff` `exists_near` `normSq_toQuaternion` `toQuaternion_sub` `toQuaternion_mul`
`star_eq` 📖	mathematical	—	`Hurwitz` `ring` `starRing` `fromQuaternion` `toQuaternion`	—	`leftInverse_fromQuaternion_toQuaternion`
`star_im_i` 📖	mathematical	—	`im_i` `Hurwitz` `ring` `starRing`	—	—
`star_im_o` 📖	mathematical	—	`im_o` `Hurwitz` `ring` `starRing`	—	—
`star_im_oi` 📖	mathematical	—	`im_oi` `Hurwitz` `ring` `starRing`	—	—
`star_re` 📖	mathematical	—	`re` `Hurwitz` `ring` `starRing` `im_o` `im_oi`	—	—
`toQuaternion_add` 📖	mathematical	—	`toQuaternion` `Hurwitz` `instAdd`	—	—
`toQuaternion_eq_zero_iff` 📖	mathematical	—	`toQuaternion` `Hurwitz` `instZero`	—	`toQuaternion_injective` `toQuaternion_zero`
`toQuaternion_injective` 📖	mathematical	—	`Hurwitz` `toQuaternion`	—	`leftInverse_fromQuaternion_toQuaternion`
`toQuaternion_intCast` 📖	mathematical	—	`toQuaternion` `Hurwitz` `instIntCast`	—	`preserves_castDef` `toQuaternion_natCast` `toQuaternion_neg`
`toQuaternion_mul` 📖	mathematical	—	`toQuaternion` `Hurwitz` `instMul`	—	—
`toQuaternion_natCast` 📖	mathematical	—	`toQuaternion` `Hurwitz` `instNatCast`	—	`preserves_unaryCast` `toQuaternion_zero` `toQuaternion_one` `toQuaternion_add`
`toQuaternion_ne_zero_iff` 📖	—	—	—	—	`toQuaternion_injective` `toQuaternion_zero`
`toQuaternion_neg` 📖	mathematical	—	`toQuaternion` `Hurwitz` `instNeg`	—	—
`toQuaternion_npow` 📖	mathematical	—	`toQuaternion` `Hurwitz` `instPowNat`	—	`preserves_npowRec` `toQuaternion_one` `toQuaternion_mul`
`toQuaternion_nsmul` 📖	mathematical	—	`toQuaternion` `Hurwitz` `instSMulNat`	—	`preserves_nsmulRec` `toQuaternion_zero` `toQuaternion_add`
`toQuaternion_one` 📖	mathematical	—	`toQuaternion` `Hurwitz` `instOne`	—	—
`toQuaternion_star` 📖	mathematical	—	`toQuaternion` `Hurwitz` `ring` `starRing`	—	—
`toQuaternion_sub` 📖	mathematical	—	`toQuaternion` `Hurwitz` `instSub`	—	`toQuaternion_neg` `toQuaternion_add`
`toQuaternion_zero` 📖	mathematical	—	`toQuaternion` `Hurwitz` `instZero`	—	—
`toQuaternion_zsmul` 📖	mathematical	—	`toQuaternion` `Hurwitz` `instSMulInt`	—	`preserves_zsmul` `toQuaternion_nsmul` `toQuaternion_neg`
`zero_im_i` 📖	mathematical	—	`im_i` `Hurwitz` `instZero`	—	—
`zero_im_o` 📖	mathematical	—	`im_o` `Hurwitz` `instZero`	—	—
`zero_im_oi` 📖	mathematical	—	`im_oi` `Hurwitz` `instZero`	—	—
`zero_re` 📖	mathematical	—	`re` `Hurwitz` `instZero`	—	—

Hurwitz.Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`castDef_negSucc` 📖	—	—	—	—	—
`castDef_ofNat` 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
`Hurwitz` 📖	CompData	60 math math: `Hurwitz.natCast_re`, `Hurwitz.neg_im_o`, `Hurwitz.mul_re`, `Hurwitz.star_im_i`, `Hurwitz.o_mul_i`, `Hurwitz.mul_im_oi`, `Hurwitz.natCast_im_i`, `Hurwitz.toQuaternion_sub`, `Hurwitz.toQuaternion_zero`, `Hurwitz.toQuaternion_zsmul`, `Hurwitz.mul_im_i`, `Hurwitz.toQuaternion_star`, `Hurwitz.left_ideal_princ`, `Hurwitz.star_im_oi`, `Hurwitz.neg_im_oi`, `Hurwitz.leftInverse_fromQuaternion_toQuaternion`, `Hurwitz.intCast_im_oi`, `Hurwitz.neg_re`, `Hurwitz.toQuaternion_mul`, `Hurwitz.norm_zero`, `HurwitzRatHat.canonicalForm`, `Hurwitz.zero_im_o`, `Hurwitz.add_im_oi`, `Hurwitz.add_re`, `Hurwitz.star_im_o`, `Hurwitz.toQuaternion_nsmul`, `Hurwitz.one_im_o`, `Hurwitz.toQuaternion_npow`, `Hurwitz.toQuaternion_intCast`, `Hurwitz.star_re`, `Hurwitz.toQuaternion_add`, `Hurwitz.zero_im_i`, `Hurwitz.zero_im_oi`, `Hurwitz.intCast_im_o`, `Hurwitz.intCast_im_i`, `Hurwitz.mul_im_o`, `Hurwitz.toQuaternion_neg`, `Hurwitz.norm_eq_mul_conj`, `Hurwitz.add_im_i`, `Hurwitz.toQuaternion_one`, `Hurwitz.natCast_im_oi`, `Hurwitz.norm_eq_zero`, `Hurwitz.leftInvOn_toQuaternion_fromQuaternion`, `Hurwitz.instCharZero`, `Hurwitz.natCast_im_o`, `Hurwitz.fromQuaternion_injOn`, `Hurwitz.add_im_o`, `Hurwitz.one_im_oi`, `Hurwitz.one_re`, `Hurwitz.star_eq`, `Hurwitz.norm_one`, `Hurwitz.toQuaternion_injective`, `Hurwitz.norm_mul`, `Hurwitz.toQuaternion_eq_zero_iff`, `Hurwitz.zero_re`, `Hurwitz.neg_im_i`, `Hurwitz.toQuaternion_natCast`, `Hurwitz.intCast_re`, `Hurwitz.quot_rem`, `Hurwitz.one_im_i`
`term𝓞` 📖	CompOp	—

---

← Back to Index