Theoremsconjugate_rpow_neg_one_half, exists_pos_algebraMap_le_iff, conjugate_le_norm_smul, conjugate_le_norm_smul', inr_mem_Icc_iff_nnnorm_le, inr_mem_Icc_iff_norm_le, instNonnegSpectrumClassComplexNonUnital, instOrderClosedTopology, inv_le_iff, inv_le_inv, inv_le_inv_iff, inv_le_one, inv_le_one_iff_one_le, isClosed_nonneg, isUnit_of_le, le_inv_iff, le_one_of_one_le_inv, mem_Icc_algebraMap_iff_nnnorm_le, mem_Icc_algebraMap_iff_norm_le, mem_Icc_iff_nnnorm_le_one, mem_Icc_iff_norm_le_one, mul_star_le_algebraMap_norm_sq, nnnorm_le_iff_of_nonneg, nnnorm_le_natCast_iff_of_nonneg, nnnorm_le_nnnorm_of_nonneg_of_le, nnnorm_le_one_iff_of_nonneg, nnnorm_mem_spectrum_of_nonneg, norm_le_iff_le_algebraMap, norm_le_natCast_iff_of_nonneg, norm_le_norm_of_nonneg_of_le, norm_le_one_iff_of_nonneg, norm_mem_spectrum_of_nonneg, norm_or_neg_norm_mem_spectrum, one_le_inv_iff_le_one, pow_antitone, pow_monotone, pow_nonneg, preimage_inr_Icc_zero_one, rpow_neg_one_le_one, rpow_neg_one_le_rpow_neg_one, star_left_conjugate_le_norm_smul, star_mul_le_algebraMap_norm_sq, star_right_conjugate_le_norm_smul, le_algebraMap_norm_self, neg_algebraMap_norm_le_self, toReal_spectralRadius_eq_norm, add_nonneg, nonneg_add, of_le, inr_le_iff, inr_nonneg_iff, instStarOrderedRing, nnreal_cfcₙ_eq_cfc_inr, cfc_nnreal_le_iff, cfc_tsub, cfcₙ_tsub, isStrictlyPositive_add, le_iff_norm_sqrt_mul_rpow, le_iff_norm_sqrt_mul_sqrt_inv | 59 |