star 📖 | CompOp | 696 mathmath: unitary.spectrum.unitary_conjugate, ContinuousMapZero.coe_star, NonUnitalSubalgebra.coe_starClosure, Quaternion.star_mul_self, Quaternion.coe_normSq_add, unitary.star_eq_inv', star_eq_zero, Quaternion.re_star, star_mul_star, QuaternionAlgebra.self_add_star, IsIdempotentElem.star_iff, Matrix.star_eq_conjTranspose, DoubleCentralizer.star_snd, differentiableOn_star_iff, norm_star, IsUnit.star, Set.image_star, star_comm_self', star_ofNat, spinGroup.star_eq_inv, Quaternion.star_smul, IsUnit.isStrictlyPositive_star_right_conjugate_iff, RingHom.star_apply, IsSelfAdjoint.star_mul_self, spinGroup.coe_star_mul_self, Unitary.conjStarAlgAut_symm, RCLike.star_def, Quaternion.star_eq_neg, BoundedContinuousFunction.mkOfCompact_star, pinGroup.coe_star_mul_self, CentroidHom.star_centerToCentroidCenter, QuaternionAlgebra.star_eq_two_re_sub, isRightRegular_star_iff, BoundedContinuousFunction.char_neg, val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe, TensorProduct.star_tmul, CliffordAlgebraQuaternion.toQuaternion_star, lp.coeFn_star, Set.star_mem_centralizer, unitary.inv_mul_mem_iff, NumberField.mem_maximalRealSubfield_iff, Complex.star_def, Matrix.isHermitian_comp_iff_forall, Subalgebra.star_adjoin_comm, LinearMap.intrinsicStar_mulRight, LE.le.star_eq, Module.End.spectrum_intrinsicStar, IsUnit.star_right_conjugate_nonneg_iff, ContinuousLinearMap.intrinsicStar_toSpanSingleton, cfc_comp_star, IsCHSHTuple.B₀_sa, spinGroup.star_eq_inv', QuaternionAlgebra.mul_star_eq_coe, commute_star_star, hasDerivAt_star_conj_iff, CFC.abs_nnrpow_two, summable_star_iff, Pi.star_mulSingle, Matrix.intrinsicStar_toLin', dotProduct_star_self_eq_zero, Matrix.posDef_iff_dotProduct_mulVec, Matrix.IsHermitian.eigenvalues_eq, LinearMap.intrinsicStar_toSpanSingleton, pinGroup.star_mul_self, ContinuousStar.continuous_star, star_dotProduct_toMatrix₂_mulVec, Complex.UnitDisc.conj_neg, Set.nonempty_star, WithCStarModule.inner_def, Matrix.star_vec, unitary.coe_star_mul_self, deriv.star, ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star, star_star, MulOpposite.op_star, Pi.star_single, Unitary.inv_mul_mem_iff, Matrix.IsUnit.posSemidef_star_right_conjugate_iff, IsCHSHTuple.B₁_sa, Pell.pellZd_sub, Set.star_centralizer, HasStrictFDerivAt.star, Memℓp.star_mem, Set.star_inv', unitary.spectrum.unitary_conjugate', unitary.mem_iff_self_mul_star, Complex.UnitDisc.im_star, HasFDerivAt.star, unitary.star_mul_self_of_mem, continuousOn_star, StarOrderedRing.lt_iff, smul_mem_closure_star_mul, CStarRing.norm_mul_self_le, Matrix.IsHermitian.apply, skewAdjoint.mem_iff, CompactlySupportedContinuousMap.star_apply, InvolutiveStar.star_involutive, Matrix.dotProduct_star_self_pos_iff, Unitization.inr_star, fderivWithin_star, IsStarNormal.star_comm_self, IsSelfAdjoint.add_star_self, IsSelfAdjoint.mul_star_self, MulChar.star_apply, Matrix.conjTranspose_eq_diagonal, Matrix.posSemidef_vecMulVec_self_star, QuaternionAlgebra.star_mul_eq_coe, Module.End.mem_eigenspace_intrinsicStar_iff, Matrix.star_dotProduct, IsLeftRegular.star, starMulAut_apply, StarOrderedRing.pos_iff, QuaternionAlgebra.star_im, Zsqrtd.im_star, StarAddMonoid.star_add, Pi.single_star, PositiveLinearMap.preGNS_norm_def, star_pos_iff, spinGroup.coe_mul_star_self, Quaternion.inv_def, eq_star_of_eq_star, CliffordAlgebra.star_def', starL_apply, StarModule.star_smul, QuaternionAlgebra.star_coe, FreeAlgebra.star_algebraMap, Pi.intrinsicStar_comul_commSemiring, CStarMatrix.conjTranspose_apply, CompactlySupportedContinuousMap.coe_star, Pell.isPell_norm, Unitary.spectrum_star_left_conjugate, MeasureTheory.MemLp.star, spinGroup.mul_star_self_of_mem, Set.star_add, Complex.UnitDisc.coe_conj, Units.mul_inv_mem_unitary, starRingAut_apply, DifferentiableAt.star_conj, Matrix.dotProduct_star, star_zsmul, eq_star_iff_eq_star, unitary.mem_iff, NonUnitalStarAlgebra.adjoin_toNonUnitalSubalgebra, Matrix.IsHermitian.ext_iff, Unitary.mem_iff_self_mul_star, Matrix.mem_unitaryGroup_iff, HasFDerivWithinAt.star, Matrix.star_dotProduct_star, star_right_conjugate_pos, CFC.abs_nnrpow, Matrix.star_vec_dotProduct_vec, MeasureTheory.AEStronglyMeasurable.star, CliffordAlgebra.star_def, Quaternion.nnnorm_star, nnnorm_star, MeasureTheory.SimpleFunc.coe_star, CFC.norm_star_mul_mul_self_of_nonneg, isStarNormal_iff, Complex.UnitDisc.conj_mul, Filter.EventuallyEq.fun_star, LinearMap.intrinsicStar_mul', differentiableAt_star_iff, NumberField.ComplexEmbedding.IsConj.eq, mul_star_self_nonneg, star_left_conjugate_pos, CentroidHom.star_apply, ContinuousLinearMap.intrinsicStar_comp, Quaternion.star_eq_two_re_sub, Unitary.expUnitary_eq_mul_inv, QuaternionAlgebra.star_smul', Matrix.star_vecMul, CStarModule.inner_smul_left_complex, Unitary.star_mul_self_of_mem, HasDerivAt.star, Quaternion.star_add_self, star_isometry, unitary.norm_sub_eq, StarRing.star_add, CStarModule.star_inner, RingQuot.Rel.star, unitary.mem_iff_star_mul_self, Pi.intrinsicStar_comul, Zsqrtd.norm_conj, CStarRing.norm_star_mul_self', Units.coe_star, Matrix.Fin.conjTranspose_circulant, RCLike.mul_wInner_left, StarMemClass.star_coe_eq, Matrix.star_apply, IsCHSHTuple.A₁_sa, PositiveLinearMap.preGNS_inner_def, differentiableAt_star_conj_iff, star_natCast_smul, starL'_apply, Unitary.coe_mul_star_self, star_intCast, LinearMap.intrinsicStar_zero, Matrix.det_conjTranspose, tendsto_star, NonUnitalSubalgebra.mem_star_iff, Unitary.mul_star_self, Unitary.spectrum_star_right_conjugate, gelfandTransform_map_star, dotProduct_star_self_nonneg, Matrix.map_star_mem_unitaryGroup_iff, FreeMonoid.star_one, StarMemClass.star_mem, pinGroup.star_mem, star_neg, FreeAlgebra.star_ι, star_ratCast_smul, Subalgebra.mem_starClosure, star_finsuppProd, MulOpposite.unop_star, QuadraticAlgebra.star_mem_nonZeroDivisors_iff, Set.star_inv, CStarRing.star_mul_self_eq_zero_iff, selfAdjoint.star_val_eq, QuadraticAlgebra.star_mk, StarHomClass.map_star, Unitization.inl_star, star_mul_self_eq_realPart_sq_add_imaginaryPart_sq, NonUnitalStarSubsemiring.star_mem', Zsqrtd.star_mk, QuaternionAlgebra.star_eq_self, star_nnrat_smul, TrivialStar.star_trivial, MeasureTheory.eLpNorm_star, NonUnitalStarAlgebra.adjoin_eq_span, ContinuousLinearMap.toLinearMap_intrinsicStar, CliffordAlgebraQuaternion.ofQuaternion_star, Matrix.conjTranspose_replicateRow, LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star, LinearMap.intrinsicStar_comp', Matrix.schur_complement_eq₂₂, DoubleCentralizer.star_fst, NormedStarGroup.norm_star_le, QuaternionAlgebra.star_add_self, CStarMatrix.star_apply, QuadraticAlgebra.mul_star, Matrix.transpose_conjTranspose, LinearMap.intrinsicStar_rTensor, LinearMap.toMatrix_innerₛₗ_apply, star_lt_one_iff, star_inv_intCast_smul, CFC.abs_nnrpow_two_mul, Matrix.PosSemidef.toLinearMap₂'_zero_iff, NormedSpace.star_exp, TensorProduct.intrinsicStar_map, unitary.star_mem, CliffordAlgebra.star_smul, pinGroup.star_eq_inv', Set.iUnion_star, CStarAlgebra.isStrictlyPositive_iff_eq_mul_star_self, HasDerivAtFilter.star, CFC.abs_star, IsUnit.isStrictlyPositive_star_left_conjugate_iff, NonUnitalStarSubalgebra.coe_centralizer, CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary, star_mul_self_add_self_mul_star, differentiableWithinAt_star_iff, star_sum, StarSubalgebra.centralizer_toSubalgebra, Filter.EventuallyEq.star, Set.union_star, IsCHSHTuple.A₀_sa, GaussianInt.toComplex_star, Circle.star_addChar, StarSubalgebra.star_mem', Ring.inverse_star, starRingEnd_apply, StarAlgebra.star_self_mem_adjoin_singleton, Unitary.star_mul_self, LinearMap.star_eq_adjoint, IsUnit.star_left_conjugate_nonneg_iff, Complex.UnitDisc.im_conj, Matrix.UnitaryGroup.inv_val, NonUnitalStarSubalgebra.mem_centralizer_iff, QuaternionAlgebra.star_add_self', Unitary.mul_inv_mem_iff, GaussianInt.div_def, isRegular_star_iff, Summable.star, Function.star_sumElim, QuadraticAlgebra.coe_norm_eq_mul_star, StarAlgebra.star_subset_adjoin, starMulEquiv_apply, star_mul_self_nonneg, QuaternionAlgebra.imK_star, Matrix.star_mul, IsUnit.isSelfAdjoint_conjugate_iff, ContinuousLinearMap.intrinsicStar_zero, star_nsmul, Unitary.conjStarAlgAut_apply, Quaternion.mul_star_eq_coe, QuadraticAlgebra.re_star, starₗᵢ_apply, isStarProjection_iff', RCLike.wInner_smul_left, Unitary.mem_iff_star_mul_self, star_right_conjugate_lt_conjugate, Subalgebra.coe_star, apply_eq_star_dotProduct_toMatrix₂_mulVec, Quaternion.normSq_add, mul_star_self_pos, ContinuousLinearMap.intrinsicStar_eq_comp, LinearMap.toMatrix'_intrinsicStar, Set.star_univ, Matrix.trace_conjTranspose, Quaternion.imI_star, Matrix.diagonal_conjTranspose, star_injective, imaginaryPart_apply_coe, Matrix.posSemidef_vecMulVec_star_self, Quaternion.imK_star, NonUnitalStarAlgebra.star_subset_adjoin, StarMulEquiv.map_star', CStarRing.norm_star_mul_self, spinGroup.mul_star_self, unitary.coe_mul_star_self, Zsqrtd.norm_eq_mul_conj, Quaternion.star_add_self', Subalgebra.starClosure_toSubalgebra, CStarModule.inner_op_smul_left, CStarMatrix.mul_entry_mul_eq_inner_toCLM, Set.compl_star, QuaternionAlgebra.coe_starAe, one_lt_star_iff, star_inv_natCast_smul, StarAlgebra.elemental.star_self_mem, star_lt_star_iff, HasFDerivAtFilter.star, IsSelfAdjoint.star_iff, Matrix.schur_complement_eq₁₁, EuclideanSpace.inner_eq_star_dotProduct, NonUnitalSubalgebra.coe_star, QuaternionAlgebra.self_add_star', star_qsmul, cfc_star_id, Unitary.symm_mulRight, Unitary.conjStarAlgAut_symm_apply, spectrum.star_mem_resolventSet_iff, selfAdjoint.star_coe_unitarySelfAddISMul, Prod.star_def, Quaternion.self_add_star', StarMemClass.coe_star, star_nnqsmul, skewAdjoint.star_val_eq, Set.Finite.star, CStarAlgebra.mul_star_le_algebraMap_norm_sq, pinGroup.mul_star_self, Quaternion.star_im, Pi.star_apply, spectrum.map_star, StarRingEquiv.map_star', Memℓp.star_iff, star_right_conjugate_le_conjugate, star_le_iff, star_eq_iff_star_eq, star_prod, MulChar.star_apply', NonUnitalStarAlgebra.elemental.star_self_mem, Set.inter_star, IsRightRegular.star, pinGroup.star_mem_iff, star_lt_iff, CFC.abs_mul_self, conjugate_lt_conjugate', ContinuousMap.star_apply, HasSum.star, isLeftRegular_star_iff, star_nnratCast, Zsqrtd.re_star, dotProduct_self_star_nonneg, LinearMap.intrinsicStar_convMul, conjugate_lt_conjugate, Complex.UnitDisc.re_star, Set.star_mem_center, spinGroup.star_mem, LinearMap.intrinsicStar_id, InnerProductSpace.toMatrix_rankOne, CliffordAlgebra.star_ι, Unitary.coe_map_star, Matrix.PosSemidef.dotProduct_mulVec_nonneg, CStarRing.norm_self_mul_star, skewAdjointPart_apply_coe, CStarAlgebra.conjugate_le_norm_smul', StarSubsemiring.star_mem', Matrix.star_eq_inv, selfAdjointPartL_apply_coe, Quaternion.self_mul_star, Matrix.mulVec_conjTranspose, StarRingEquivClass.map_star, QuadraticAlgebra.star_mem_nonZeroDivisors, ContinuousLinearMap.intrinsicStar_smulRight, LinearMap.intrinsicStar_mulLeft, one_le_star_iff, CStarAlgebra.star_mul_le_algebraMap_norm_sq, SemiconjBy.star_star_star, Quaternion.inner_def, Zsqrtd.mul_star, Matrix.posSemidef_iff_eq_sum_vecMulVec, Matrix.vecMul_conjTranspose, StarAlgebra.adjoin_toSubalgebra, LinearMap.intrinsicStar_lTensor, QuaternionAlgebra.im_star, unitary.coe_map_star, Set.Nonempty.star, conjugate_pos', star_zero, NonUnitalSubalgebra.star_mono, Pi.star_def, CStarAlgebra.star_left_conjugate_le_norm_smul, StarOrderedRing.le_iff, ContinuousWithinAt.star, MeasureTheory.AEEqFun.coeFn_star, Quaternion.im_star, coe_starₗᵢ, Set.star_subset, Matrix.star_dotProduct_gram_mulVec, MulChar.star_eq_inv, Subalgebra.topologicalClosure_star_comm, StarSubalgebra.coe_centralizer_centralizer, Pell.isPell_star, isSelfAdjoint_conjugate_iff_of_isUnit', Subalgebra.star_mem_star_iff, Quaternion.coe_starAe, toMatrix_innerSL_apply, LinearMap.intrinsicStar_single, Matrix.PosSemidef.re_dotProduct_nonneg, IsStarNormal.star, LinearMap.intrinsicStar_smulRight, star_id_of_comm, star_left_conjugate_le_conjugate, NonUnitalStarSubalgebra.coe_centralizer_centralizer, Filter.IsIncreasingApproximateUnit.eventually_star_eq, Matrix.posSemidef_iff_dotProduct_mulVec, CStarAlgebra.nonneg_iff_eq_star_mul_self, pinGroup.star_mul_self_of_mem, DifferentiableAt.star_star, Filter.Tendsto.star, NonUnitalStarSubalgebra.centralizer_toNonUnitalSubalgebra, Quaternion.self_add_star, Quaternion.normSq_def, ContinuousLinearMap.intrinsicStar_comp', skewAdjoint.conjugate', StarOrderedRing.nonneg_iff, cfc_unitary_iff, ContinuousLinearMap.intrinsicStar_id, Matrix.conjTranspose_apply, Matrix.PosSemidef.dotProduct_mulVec_zero_iff, HasDerivWithinAt.star, CliffordAlgebra.star_algebraMap, BoundedContinuousFunction.star_mem_range_charAlgHom, cfcₙ_norm_sq_nonneg, Function.update_star, StarSubalgebra.mem_centralizer_iff, selfAdjointPart_apply_coe, skewAdjointPartL_apply_coe, BoundedContinuousFunction.star_apply, star_div, RingHom.star_def, ContinuousMap.coe_star, Quaternion.star_mul_eq_coe, IsSelfAdjoint.star_add_self, star_left_conjugate_lt_conjugate, Matrix.isSymm_iff_intrinsicStar_toLin', Matrix.specialUnitaryGroup.coe_star, Complex.UnitDisc.re_conj, Complex.UnitDisc.conj_conj, conjugate_nonneg', BoundedContinuousFunction.coe_star, Unitary.norm_sub_eq, CStarAlgebra.nonneg_iff_eq_mul_star_self, pinGroup.star_eq_inv, QuaternionAlgebra.imJ_star, CStarAlgebra.conjugate_le_norm_smul, unitary.coe_star, CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self, ContinuousOn.star, Matrix.mem_unitaryGroup_iff', Set.star_singleton, Unitary.mul_star_self_of_mem, NonUnitalStarSubalgebra.star_mem', selfAdjoint.mem_iff, Matrix.updateCol_conjTranspose, unitary.mul_inv_mem_iff, CFC.abs_sq, LinearMap.intrinsicStar_apply, Subalgebra.coe_starClosure, Unitization.snd_star, FreeMonoid.star_of, DifferentiableAt.star, LinearMap.isSelfAdjoint_iff_map_star, StarMul.star_mul, Set.mem_star, Set.star_mem_star, CStarMatrix.star_apply_of_isSelfAdjoint, QuaternionAlgebra.re_star, continuousAt_star, Set.star_subset_star, Set.star_mem_centralizer', ContinuousLinearMap.star_eq_adjoint, star_star_mul, CStarAlgebra.isStrictlyPositive_TFAE, derivWithin.star, isSelfAdjoint_iff, star_mul_self_sub_self_mul_star, fderiv_star, cfcₙ_star, SubStarSemigroup.star_mem', star_sub, IsIdempotentElem.star, unitary.expUnitary_eq_mul_inv, star_le_one_iff, Commute.star_right, ZeroAtInftyContinuousMap.star_apply, skewAdjoint.conjugate, NonUnitalStarAlgebra.star_self_mem_adjoin_singleton, StarSubalgebra.coe_centralizer, Matrix.conjTranspose_smul_non_comm, Unitary.symm_mulLeft, CStarMatrix.star_eq_conjTranspose, Unitary.mem_iff, intrinsicStar_def, Subalgebra.mem_star_iff, tsum_star, Matrix.conjTranspose_single, spinGroup.star_mul_self_of_mem, deriv_star_conj, star_right_conjugate_nonneg, LinearIsometryEquiv.star_eq_symm, Matrix.conjTranspose_vecMulVec, Units.embed_product_star, Module.End.isUnit_intrinsicStar_iff, Unitary.symm_mulRight_apply, Matrix.UnitaryGroup.map_star_coe, QuaternionAlgebra.star_smul, StarAlgebra.adjoin_eq_span, Matrix.conjTranspose_transpose, QuadraticAlgebra.norm_star, Unitization.norm_splitMul_snd_sq, Matrix.IsHermitian.star_mul_self_mul_eq_diagonal, Unitary.star_eq_inv, EuclideanSpace.inner_toLp_toLp, realPart_apply_coe, starLinearEquiv_apply, dotProduct_self_star_eq_zero, commute_star_comm, star_finsuppSum, QuadraticAlgebra.algebraMap_norm_eq_mul_star, Complex.UnitDisc.star_neg, conjugate_pos, Units.coe_star_inv, DifferentiableOn.star, star_zpow, Matrix.IsUnit.posSemidef_star_left_conjugate_iff, pinGroup.coe_star, Matrix.conjTranspose_smul, star_nonpos_iff, differentiable_star_iff, CStarAlgebra.star_right_conjugate_le_norm_smul, Complex.UnitDisc.star_eq_zero, Unitary.symm_mulLeft_apply, Continuous.star, LinearMap.isSymm_iff_basis, star_inj, starContinuousMap_apply, Prod.snd_star, CStarRing.nnnorm_self_mul_star, Complex.UnitDisc.star_zero, starRingEquiv_apply, CStarAlgebra.nonneg_TFAE, Matrix.updateRow_conjTranspose, pinGroup.coe_mul_star_self, summable_star_iff', cfcₙ_star_id, CFC.abs_mul_abs, star_natCast, lp.star_apply, LinearMap.intrinsicStar_comp, IsRegular.star, ContinuousAt.star, Quaternion.imJ_star, isUnit_star, star_div₀, star_le_star_iff, star_mul', star_zpow₀, conjugate_le_conjugate', Unitary.coe_star_mul_self, star_mul_self_pos, TensorProduct.star_map_apply_eq_map_intrinsicStar, CFC.norm_mul_mul_star_self_of_nonneg, cfc_star, IsUnit.mem_unitary_iff_mul_star_self, star_ratCast, Unitary.star_mem_iff, star_invOf, StarMonoidHom.map_star', Commute.star_left, Matrix.conjTranspose_smul_self, StarAlgHom.map_star', NonUnitalSubalgebra.starClosure_toNonUnitalSubalgebra, Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary, Set.iInter_star, unitary.mul_star_self, spinGroup.coe_star, Prod.fst_star, unitary.star_mem_iff, MeasureTheory.AEEqFun.eLpNorm_star, NonUnitalStarAlgHom.map_star', star_nonneg_iff, starAddEquiv_apply, Complex.UnitDisc.coe_star, Unitary.coe_star, ContinuousLinearMap.intrinsicStar_apply, deriv.star', IsSelfAdjoint.conjugate, Set.star_empty, cfcₙ_comp_star, Subalgebra.star_mono, HasFDerivAt.star_star, Matrix.UnitaryGroup.star_mul_self, Matrix.conjTranspose_circulant, star_mem_iff, Unitary.conjStarAlgAut_star_apply, QuaternionAlgebra.imI_star, conjugate_nonneg, IsSelfAdjoint.conjugate', NonUnitalStarRingHom.map_star', IsSelfAdjoint.star_eq, Module.End.IsUnit.intrinsicStar, QuaternionAlgebra.star_mk, unitary.star_eq_inv, Quaternion.normSq_star, Unitization.fst_star, CStarRing.mul_star_self_eq_zero_iff, QuaternionAlgebra.star_eq_neg, Matrix.IsUnit.posDef_star_left_conjugate_iff, star_rat_smul, CStarRing.nnnorm_star_mul_self, star_left_conjugate_nonneg, isIdempotentElem_star_mul_self_iff_isIdempotentElem_self_mul_star, Unitary.star_eq_inv', Differentiable.star, Matrix.IsHermitian.star_eigenvectorUnitary_mulVec, InnerProductSpace.symm_toEuclideanLin_rankOne, MeasureTheory.Lp.coeFn_star, QuadraticAlgebra.im_star, NonUnitalSubalgebra.mem_starClosure, semiconjBy_star_star_star, Unitary.star_mem, IsUnit.mem_unitary_iff_star_mul_self, LinearMap.intrinsicStar_eq_comp, Unitary.path_apply, HasDerivAt.star_conj, star_one, Set.star_mul, star_inv, Matrix.diag_conjTranspose, Quaternion.star_coe, PositiveLinearMap.preGNS_norm_sq, pinGroup.mul_star_self_of_mem, Matrix.conjTranspose_replicateCol, IsUnit.isSelfAdjoint_conjugate_iff', unitary.star_mul_self, continuousWithinAt_star, Units.inv_mul_mem_unitary, DifferentiableWithinAt.star, Matrix.dotProduct_self_star_pos_iff, star_inv₀, conjugate_le_conjugate, star_neg_iff, Set.star_preimage, Matrix.IsHermitian.im_star_dotProduct_mulVec_self, MeasureTheory.StronglyMeasurable.star, Matrix.PosDef.dotProduct_mulVec_pos, algebraMap_star_comm, Matrix.UnitaryGroup.inv_apply, Matrix.IsUnit.posDef_star_right_conjugate_iff, spinGroup.star_mul_self, Matrix.PosDef.re_dotProduct_pos, spinGroup.star_mem_iff, ZeroAtInftyContinuousMap.coe_star, Quaternion.star_eq_self, unitary.mul_star_self_of_mem, NonUnitalSubalgebra.star_mem_star_iff, isSelfAdjoint_conjugate_iff_of_isUnit, Matrix.star_mulVec, Commute.star_star, HasStrictDerivAt.star, star_pow, Quaternion.norm_star, star_intCast_smul, NonUnitalSubalgebra.star_adjoin_comm
|