DefinitionsinstReprQuaternionAlgebra, algebra, equivProd, equivTuple, im, instCoeTC, instDistribMulAction, instDivisionRing, instGroupWithZero, instInhabited, instInv, instModule, instMulAction, instNNRatCast, instRatCast, instRing, instSMul, instStar, instStarRing, normSq, starAe, Β«termβ[_,_,_,_]Β», Β«termβ[_,_,_]Β», Β«termβ[_]Β», QuaternionAlgebra, addEquivProd, addEquivTuple, basisOneIJK, equivProd, equivTuple, im, imI, imIβ, imJ, imJβ, imK, imKβ, instAdd, instAddCommGroup, instAddCommGroupWithOne, instAlgebra, instCoeTC, instDistribMulAction, instInhabited, instModule, instMul, instMulAction, instNeg, instOne, instRing, instSMul, instStarQuaternionAlgebra, instStarRing, instSub, instZero, linearEquivTuple, re, reβ, starAe, swapEquiv | 60 |
Theoremsmk_quaternion, mk_quaternionAlgebra, mk_quaternionAlgebra_of_infinite, mk_quaternion_of_infinite, mk_univ_quaternion, mk_univ_quaternionAlgebra, mk_univ_quaternionAlgebra_of_infinite, mk_univ_quaternion_of_infinite, algebraMap_def, algebraMap_injective, coe_add, coe_commute, coe_commutes, coe_div, coe_inj, coe_injective, coe_intCast, coe_inv, coe_mul, coe_mul_eq_smul, coe_natCast, coe_neg, coe_nnratCast, coe_normSq_add, coe_one, coe_pow, coe_ratCast, coe_smul, coe_starAe, coe_sub, coe_zero, coe_zpow, eq_re_iff_mem_range_coe, eq_re_of_eq_coe, equivProd_apply, equivTuple_apply, equivTuple_symm_apply, ext, ext_iff, finrank_eq_four, imI_add, imI_coe, imI_equivProd_symm_apply, imI_im, imI_intCast, imI_mul, imI_natCast, imI_neg, imI_nnratCast, imI_one, imI_ratCast, imI_smul, imI_star, imI_sub, imI_zero, imJ_add, imJ_coe, imJ_equivProd_symm_apply, imJ_im, imJ_intCast, imJ_mul, imJ_natCast, imJ_neg, imJ_nnratCast, imJ_one, imJ_ratCast, imJ_smul, imJ_star, imJ_sub, imJ_zero, imK_add, imK_coe, imK_equivProd_symm_apply, imK_im, imK_intCast, imK_mul, imK_natCast, imK_neg, imK_nnratCast, imK_one, imK_ratCast, imK_smul, imK_star, imK_sub, imK_zero, im_add, im_coe, im_idem, im_intCast, im_natCast, im_neg, im_nnratCast, im_one, im_ratCast, im_smul, im_sq, im_star, im_sub, im_zero, instFinite, instFree, instIsDomain, instIsScalarTower, instIsStarNormal, instNoZeroDivisors, instNontrivial, instSMulCommClass, inv_def, mul_coe_eq_smul, mul_star_eq_coe, normSq_add, normSq_coe, normSq_def, normSq_def', normSq_div, normSq_eq_zero, normSq_intCast, normSq_inv, normSq_le_zero, normSq_natCast, normSq_ne_zero, normSq_neg, normSq_nonneg, normSq_ratCast, normSq_smul, normSq_star, normSq_zpow, rank_eq_four, re_add, re_add_im, re_coe, re_equivProd_symm_apply, re_im, re_intCast, re_mul, re_natCast, re_neg, re_nnratCast, re_one, re_ratCast, re_smul, re_star, re_sub, re_zero, self_add_star, self_add_star', self_mul_star, smul_coe, sq_eq_neg_normSq, sq_eq_normSq, star_add_self, star_add_self', star_coe, star_eq_neg, star_eq_self, star_eq_two_re_sub, star_im, star_mul_eq_coe, star_mul_self, star_smul, sub_im_self, sub_re_self, algebraMap_eq, algebraMap_injective, coe_add, coe_addEquivProd, coe_addEquivTuple, coe_algebraMap, coe_basisOneIJK_repr, coe_commute, coe_commutes, coe_inj, coe_injective, coe_intCast, coe_linearEquivTuple, coe_linearEquivTuple_symm, coe_mul, coe_mul_eq_smul, coe_natCast, coe_neg, coe_ofNat, coe_one, coe_pow, coe_smul, coe_starAe, coe_sub, coe_symm_addEquivProd, coe_symm_addEquivTuple, coe_zero, comm, eq_re_iff_mem_range_coe, eq_re_of_eq_coe, equivProd_apply, equivTuple_apply, equivTuple_symm_apply, ext, ext_iff, finrank_eq_four, imI_add, imI_coe, imI_equivProd_symm_apply, imI_im, imI_intCast, imI_mul, imI_natCast, imI_neg, imI_ofNat, imI_one, imI_smul, imI_star, imI_sub, imI_swapEquiv_apply, imI_swapEquiv_symm_apply, imI_zero, imIβ_apply, imJ_add, imJ_coe, imJ_equivProd_symm_apply, imJ_im, imJ_intCast, imJ_mul, imJ_natCast, imJ_neg, imJ_ofNat, imJ_one, imJ_smul, imJ_star, imJ_sub, imJ_swapEquiv_apply, imJ_swapEquiv_symm_apply, imJ_zero, imJβ_apply, imK_add, imK_coe, imK_equivProd_symm_apply, imK_im, imK_intCast, imK_mul, imK_natCast, imK_neg, imK_ofNat, imK_one, imK_smul, imK_star, imK_sub, imK_swapEquiv_apply, imK_swapEquiv_symm_apply, imK_zero, imKβ_apply, im_add, im_coe, im_idem, im_intCast, im_natCast, im_neg, im_ofNat, im_one, im_smul, im_star, im_sub, im_zero, instFinite, instFree, instIsScalarTower, instIsStarNormal, instIsTorsionFree, instNontrivial, instSMulCommClass, instSubsingleton, eta, mk_add_mk, mk_mul_mk, mk_sub_mk, mul_coe_eq_smul, mul_star_eq_coe, neg_mk, rank_eq_four, re_add, re_add_im, re_coe, re_equivProd_symm_apply, re_im, re_intCast, re_mul, re_natCast, re_neg, re_ofNat, re_one, re_smul, re_star, re_sub, re_swapEquiv_apply, re_swapEquiv_symm_apply, re_zero, reβ_apply, self_add_star, self_add_star', smul_coe, smul_mk, star_add_self, star_add_self', star_coe, star_eq_neg, star_eq_self, star_eq_two_re_sub, star_im, star_mk, star_mul_eq_coe, star_smul, star_smul', sub_im_self, sub_re_self, instNontrivialQuaternion, instSubsingletonQuaternion | 314 |