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, add_im, add_imI, add_imJ, add_imK, add_re, algebraMap_def, algebraMap_injective, coe_add, coe_commute, coe_commutes, coe_div, coe_im, coe_imI, coe_imJ, coe_imK, 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_re, 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_imI, im_imJ, im_imK, im_intCast, im_natCast, im_neg, im_nnratCast, im_one, im_ratCast, im_re, im_smul, im_sq, im_star, im_sub, im_zero, instFinite, instFree, instIsDomain, instIsScalarTower, instIsStarNormal, instNoZeroDivisors, instNontrivial, instSMulCommClass, intCast_im, intCast_imI, intCast_imJ, intCast_imK, intCast_re, inv_def, mul_coe_eq_smul, mul_imI, mul_imJ, mul_imK, mul_re, mul_star_eq_coe, natCast_im, natCast_imI, natCast_imJ, natCast_imK, natCast_re, neg_im, neg_imI, neg_imJ, neg_imK, neg_re, 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, one_im, one_imI, one_imJ, one_imK, one_re, rank_eq_four, ratCast_im, ratCast_imI, ratCast_imJ, ratCast_imK, ratCast_re, 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, smul_im, smul_imI, smul_imJ, smul_imK, smul_re, 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_imI, star_imJ, star_imK, star_mul_eq_coe, star_mul_self, star_re, star_smul, sub_im, sub_imI, sub_imJ, sub_imK, sub_im_self, sub_re, sub_re_self, sub_self_im, sub_self_re, zero_im, zero_imI, zero_imJ, zero_imK, zero_re, add_im, algebraMap_eq, algebraMap_injective, coe_add, coe_addEquivProd, coe_addEquivTuple, coe_algebraMap, coe_basisOneIJK_repr, coe_commute, coe_commutes, coe_im, coe_imI, coe_imJ, coe_imK, 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_re, 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_imI, im_imJ, im_imK, im_intCast, im_natCast, im_neg, im_ofNat, im_one, im_re, im_smul, im_star, im_sub, im_zero, instFinite, instFree, instIsScalarTower, instIsStarNormal, instIsTorsionFree, instNontrivial, instSMulCommClass, instSubsingleton, intCast_im, intCast_imI, intCast_imJ, intCast_imK, intCast_re, eta, mk_add_mk, mk_mul_mk, mk_sub_mk, mul_coe_eq_smul, mul_star_eq_coe, natCast_im, natCast_imI, natCast_imJ, natCast_imK, natCast_re, neg_im, neg_mk, ofNat_im, ofNat_imI, ofNat_imJ, ofNat_imK, ofNat_re, one_im, 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_im, 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, sub_im_self, sub_re_self, sub_self_im, sub_self_re, zero_im, instNontrivialQuaternion, instSubsingletonQuaternion | 410 |