Quaternion 📖 | CompOp | 257 mathmath: Quaternion.normSq_eq_zero, Quaternion.star_mul_self, Quaternion.coe_normSq_add, Quaternion.star_imJ, Quaternion.re_star, Quaternion.add_imJ, Quaternion.instSMulCommClass, Quaternion.add_imK, Quaternion.im_add, Quaternion.snd_imJ_dualNumberEquiv_symm, Quaternion.imI_zero, Quaternion.coe_natCast, Quaternion.instNoZeroDivisors, Quaternion.neg_re, Quaternion.star_smul, Quaternion.imI_sub, Quaternion.one_imI, Quaternion.rank_eq_four, Quaternion.star_eq_neg, Quaternion.finrank_eq_four, Quaternion.imK_equivProd_symm_apply, Quaternion.intCast_imK, Quaternion.continuous_imI, Quaternion.coeComplex_mul, Quaternion.star_imI, Quaternion.coe_inv, Quaternion.normSq_natCast, Quaternion.im_intCast, Quaternion.imJ_smul, Quaternion.imK_natCast, instNontrivialQuaternion, Quaternion.add_re, Quaternion.imI_mul, Quaternion.snd_re_dualNumberEquiv_symm, Quaternion.coe_ratCast, Quaternion.imJ_one, Quaternion.coe_pow, Quaternion.ratCast_re, Quaternion.imJ_fst_dualNumberEquiv, Quaternion.mul_imK, Quaternion.star_re, Quaternion.coe_commutes, Quaternion.imJ_zero, Quaternion.instFree, Quaternion.sub_imJ, Quaternion.im_smul, Quaternion.imI_fst_dualNumberEquiv, Quaternion.im_zero, Quaternion.instCStarRingReal, Quaternion.algebraMap_def, Quaternion.normSq_smul, Quaternion.re_equivProd_symm_apply, Quaternion.linearIsometryEquivTuple_symm_apply, Quaternion.smul_imK, Quaternion.normSq_le_zero, Quaternion.inv_def, Quaternion.zero_imJ, Quaternion.smul_im, Quaternion.normSq_nonneg, Quaternion.instNontrivial, Quaternion.coe_zpow, Quaternion.im_one, Quaternion.imJ_nnratCast, Quaternion.re_zero, Quaternion.nnnorm_star, Quaternion.re_add_im, Quaternion.fst_imK_dualNumberEquiv_symm, Quaternion.coe_zero, Quaternion.star_eq_two_re_sub, Quaternion.coeComplex_add, Quaternion.one_im, Quaternion.im_natCast, Quaternion.star_add_self, Quaternion.sub_re_self, Quaternion.add_imI, Quaternion.expSeries_odd_of_imaginary, Quaternion.smul_coe, Quaternion.instIsDomain, Quaternion.continuous_imJ, Quaternion.neg_imJ, Quaternion.coe_smul, Quaternion.imI_neg, Quaternion.mul_re, Quaternion.coeComplex_zero, Quaternion.imI_nnratCast, Quaternion.imK_fst_dualNumberEquiv, Quaternion.imK_nnratCast, Quaternion.instCompleteSpaceReal, Quaternion.re_fst_dualNumberEquiv, Quaternion.imK_zero, Quaternion.norm_coe, Quaternion.sub_self_im, Quaternion.one_imK, Quaternion.normSq_inv, Quaternion.exp_of_re_eq_zero, Quaternion.equivProd_apply, Quaternion.im_coe, Quaternion.re_exp, Quaternion.algebraMap_injective, Quaternion.normSq_eq_norm_mul_self, Quaternion.imJ_neg, Quaternion.expSeries_even_of_imaginary, Quaternion.sub_self_re, Quaternion.intCast_imI, Quaternion.fst_imJ_dualNumberEquiv_symm, Quaternion.equivTuple_apply, Quaternion.zero_imK, Quaternion.imK_mul, Quaternion.coe_div, Quaternion.intCast_imJ, Quaternion.mul_star_eq_coe, Quaternion.fst_imI_dualNumberEquiv_symm, instSubsingletonQuaternion, Quaternion.normSq_add, Quaternion.neg_im, Quaternion.imI_star, Quaternion.imI_smul, Quaternion.imK_star, Quaternion.normSq_exp, Quaternion.star_add_self', Quaternion.sub_im, Quaternion.im_exp, Quaternion.re_one, Quaternion.zero_re, Quaternion.smul_re, Quaternion.self_add_star', Quaternion.coe_mul_eq_smul, Quaternion.instIsStarNormal, Quaternion.summable_coe, Quaternion.zero_imI, Quaternion.sub_imI, Quaternion.imJ_snd_dualNumberEquiv, Quaternion.star_im, Quaternion.re_natCast, Quaternion.snd_imK_dualNumberEquiv_symm, Quaternion.sq_eq_neg_normSq, Quaternion.imK_neg, Quaternion.coe_one, Quaternion.imK_ratCast, Quaternion.tsum_coe, Quaternion.continuous_im, Quaternion.sq_eq_normSq, Quaternion.imJ_mul, Quaternion.im_nnratCast, Quaternion.coe_sub, Quaternion.natCast_im, Quaternion.self_mul_star, Quaternion.imJ_ratCast, Quaternion.im_neg, Quaternion.neg_imK, Quaternion.imK_intCast, Quaternion.inner_def, Quaternion.normSq_def', Quaternion.imI_add, Quaternion.ratCast_im, Quaternion.imK_smul, Quaternion.star_imK, Quaternion.im_star, Quaternion.coe_mul, Quaternion.ratCast_imI, Quaternion.imJ_equivProd_symm_apply, Quaternion.normSq_zpow, Quaternion.coe_nnratCast, Quaternion.coe_starAe, Quaternion.sub_im_self, Quaternion.inner_self, Quaternion.norm_exp, Quaternion.self_add_star, Quaternion.normSq_def, Quaternion.continuous_coe, Quaternion.imK_one, Quaternion.ratCast_imK, Quaternion.coe_commute, Quaternion.coe_injective, Quaternion.ratCast_imJ, Quaternion.re_neg, Quaternion.imI_intCast, Quaternion.star_mul_eq_coe, Quaternion.normSq_neg, Quaternion.one_imJ, Quaternion.re_snd_dualNumberEquiv, Quaternion.re_add, Quaternion.mul_coe_eq_smul, Quaternion.im_ratCast, Quaternion.imJ_add, Quaternion.im_sub, Quaternion.imI_natCast, Quaternion.snd_imI_dualNumberEquiv_symm, Quaternion.add_im, Quaternion.sub_re, Quaternion.imI_equivProd_symm_apply, Quaternion.coe_intCast, Cardinal.mk_univ_quaternion_of_infinite, Cardinal.mk_quaternion, Quaternion.re_smul, Quaternion.eq_re_iff_mem_range_coe, Quaternion.coe_add, Quaternion.normSq_intCast, Quaternion.natCast_imK, Quaternion.coe_ofComplex, Quaternion.re_sub, Quaternion.mul_imI, Quaternion.re_ratCast, Quaternion.intCast_re, Quaternion.coe_im, Quaternion.zero_im, Quaternion.instNormOneClassReal, Quaternion.instIsScalarTower, Quaternion.imJ_star, Quaternion.equivTuple_symm_apply, Quaternion.linearIsometryEquivTuple_apply, Cardinal.mk_quaternion_of_infinite, Quaternion.sub_imK, Quaternion.im_sq, Quaternion.imJ_natCast, Quaternion.natCast_imJ, Cardinal.mk_univ_quaternion, Quaternion.coe_neg, Quaternion.coeComplex_one, Quaternion.hasSum_coe, Quaternion.intCast_im, Quaternion.hom_ext_iff, Quaternion.continuous_imK, Quaternion.re_intCast, Quaternion.re_mul, Quaternion.normSq_div, Quaternion.instFinite, Quaternion.coe_real_complex_mul, Quaternion.normSq_star, Quaternion.imK_sub, Quaternion.normSq_ratCast, Quaternion.imK_add, Quaternion.fst_re_dualNumberEquiv_symm, Quaternion.continuous_normSq, Quaternion.continuous_re, Quaternion.imI_snd_dualNumberEquiv, Quaternion.imJ_intCast, Quaternion.smul_imJ, Quaternion.one_re, Quaternion.exp_coe, Quaternion.star_coe, Quaternion.smul_imI, Quaternion.norm_toLp_equivTuple, Quaternion.imI_one, Quaternion.exp_eq, Quaternion.imJ_sub, Quaternion.normSq_coe, Quaternion.re_nnratCast, Quaternion.natCast_imI, Quaternion.nnnorm_coe, Quaternion.mul_imJ, Quaternion.star_eq_self, Quaternion.imK_snd_dualNumberEquiv, Quaternion.neg_imI, Quaternion.imI_ratCast, Quaternion.natCast_re, Quaternion.norm_star
|