spectrum 📖 | CompOp | 188 mathmath: unitary.spectrum.unitary_conjugate, spectrum.inv_mem_iff, quasispectrum_eq_spectrum_union, spectrum_subset_quasispectrum, Matrix.IsHermitian.isClosedEmbedding_cfcAux, IsometricContinuousFunctionalCalculus.isGreatest_nnnorm_spectrum, IsSelfAdjoint.commute_cfcHom, Subalgebra.spectrum_sUnion_connectedComponentIn, Module.End.HasEigenvalue.mem_spectrum, spectrum.subset_closedBall_norm_mul, spectrumRestricts_iff, spectrum.instCompactSpace, Matrix.spectrum_toEuclideanLin, spectrum.inv₀_mem_iff, ContinuousFunctionalCalculus.compactSpace_spectrum, Module.End.spectrum_intrinsicStar, CStarAlgebra.norm_or_neg_norm_mem_spectrum, Matrix.spectrum_toLpLin, StarAlgebra.elemental.characterSpaceToSpectrum_coe, WeakDual.CharacterSpace.apply_mem_spectrum, Matrix.mem_spectrum_iff_isRoot_charpoly, cfcHom_continuous, cfcL_apply, LinearMap.spectrum_toMatrix', spectrum.nonempty_of_isAlgClosed_of_finiteDimensional, cfcHom_nonneg_iff, cfc_apply_mkD, spectrum_diagonal, unitary.spectrum.unitary_conjugate', AlgHom.apply_mem_spectrum, NNReal.spectrum_nonempty, cfcHom_isClosedEmbedding, SpectrumRestricts.compactSpace, Pi.spectrum_eq, spectrum.zero_notMem_iff, ContinuousFunctionalCalculus.isCompact_spectrum, IsIdempotentElem.spectrum_subset, cfcHom_le_iff, cfcHom_id, Unitary.spectrum_star_left_conjugate, IsSelfAdjoint.coe_mem_spectrum_complex, spectrum.zero_mem_iff, spectrum.gelfandTransform_eq, spectrum.zero_mem, spectrum.zero_notMem, ContinuousMap.spectrum_eq_preimage_range, Matrix.mem_spectrum_of_isRoot_charpoly, Unitary.norm_sub_one_lt_two_iff, spectrum.isCompact, spectrum.algebraMap_mem_iff, CFC.spectrum_algebraMap_eq, SpectrumRestricts.algebraMap_image, continuousOn_cfc_setProd, spectrum.smul_mem_smul_iff, Matrix.finite_spectrum, IsSelfAdjoint.val_re_map_spectrum, Unitization.zero_mem_spectrum_inr, Module.End.hasUnifEigenvalue_iff_mem_spectrum, coe_mem_spectrum_real_of_nonneg, Prod.spectrum_eq, IsSelfAdjoint.isConnected_spectrum_compl, spectrum.one_eq, Matrix.instFiniteSpectrum, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, Unitary.spectrum_star_right_conjugate, continuousOn_cfc_nnreal, spectrum.map_pow, ContinuousFunctionalCalculus.exists_cfc_of_predicate, spectrum.pow_image_subset, spectrum.units_conjugate, Units.continuousOn_zpow₀_spectrum, spectrum.subset_subalgebra, cfc_def, IsSelfAdjoint.spectrum_nonempty, lipschitzOnWith_cfc_fun, StarSubalgebra.spectrum_eq, spectrum.inv₀_mem_inv_iff, SpectrumRestricts.subset_preimage, Matrix.IsHermitian.cfcAux_apply, spectrum.preimage_algebraMap, Matrix.instFiniteElemRealSpectrum, unitary.spectrum_subset_circle, spectrum.isClosed, mem_quasispectrum_iff, LinearMap.spectrum_toMatrix, spectrum.isBounded, Unitization.mem_spectrum_inr_of_not_isUnit, Subalgebra.frontier_subset_frontier, spectrum.exists_mem_of_not_isUnit_aeval_prod, spectrum.subset_singleton_zero_compl, AlgEquiv.spectrum_eq, spectrum.nonempty, spectrum_subset_unitary_of_mem_unitary, spectrum.add_singleton_eq, cfc_eq_cfcL_mkD, range_cfc_eq_range_cfcHom, NormedRing.algEquivComplexOfComplete_symm_apply, Matrix.IsHermitian.spectrum_eq_image_range, Unitary.spectrum_subset_slitPlane_iff_norm_lt_two, spectrum.singleton_add_eq, spectrum.singleton_sub_eq, spectrum.map_star, Module.End.finite_spectrum, upperHemicontinuous_spectrum_nnreal, spec_cfcₙAux, cfcHom_eq_cfc_extend, spectrum.subset_polynomial_aeval, Matrix.spectrum_toLin, SpectrumRestricts.starAlgHom_apply, Matrix.finite_real_spectrum, spectrum.map_inv, Commute.cfcHom, AlgHom.spectrum_apply_subset, spectrum.mem_iff, spectrum.add_mem_add_iff, spectrum.map_polynomial_aeval_of_degree_pos, ContinuousMap.spectrum_eq_range, StarSubalgebra.mem_spectrum_iff, Matrix.IsHermitian.spectrum_real_eq_range_eigenvalues, cfcHom_isStrictlyPositive_iff, WeakDual.CharacterSpace.mem_spectrum_iff_exists, spectrum.add_mem_iff, CFC.spectrum_abs, Units.continuousOn_inv₀_spectrum, Units.zero_notMem_spectrum, cfc_apply_pi, SpectrumRestricts.image, spectrum.units_conjugate', IsSelfAdjoint.map_spectrum_real, Matrix.IsHermitian.cfcAux_id, spectrum.scalar_eq, unitary_iff_isStarNormal_and_spectrum_subset_unitary, spectrum.of_subsingleton, Subalgebra.frontier_spectrum, spectrum.setOf_isUnit_inter_mul_comm, Unitization.quasispectrum_eq_spectrum_inr', spectrum.isCompact_nnreal, spectrum.unit_mem_mul_comm, selfAdjoint.val_re_map_spectrum, Matrix.IsHermitian.eigenvalues_mem_spectrum_real, cfcHom_predicate, spectrum.instCompactSpaceNNReal, spectrum.preimage_units_mul_comm, norm_cfcHom, spectrum.exists_nnnorm_eq_spectralRadius, unitary.norm_sub_one_lt_two_iff, spectrum.nonzero_mul_comm, quasispectrum_eq_spectrum_union_zero, continuousOn_cfc_nnreal_setProd, SpectrumRestricts.rightInvOn, range_cfcHom, Module.End.mem_spectrum_iff_isRoot_charpoly, nnnorm_cfcHom, continuousOn_cfc, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, spectrum.neg_eq, CStarAlgebra.norm_mem_spectrum_of_nonneg, Module.End.hasEigenvalue_iff_mem_spectrum, CFC.spectrum_one_eq, IsometricContinuousFunctionalCalculus.isGreatest_norm_spectrum, spectrum.unit_smul_eq_smul, CFC.spectrum_nonempty, CFC.spectrum_algebraMap_subset, IsometricContinuousFunctionalCalculus.isometric, spectrum.map_polynomial_aeval, ContinuousFunctionalCalculus.spectrum_nonempty, Unitization.quasispectrum_eq_spectrum_inr, spectrum.map_pow_of_pos, cfcHom_eq_of_isStarNormal, upperHemicontinuous_spectrum, cfcHom_map_spectrum, spectrum.zero_eq, spectrum.subset_circle_of_unitary, spectrum.subset_closedBall_norm, spectrum.vadd_eq, IsometricContinuousFunctionalCalculus.isGreatest_spectrum, Module.End.HasUnifEigenvalue.mem_spectrum, continuousFunctionalCalculus_map_id, spectrum.sub_singleton_eq, CStarAlgebra.nnnorm_mem_spectrum_of_nonneg, Unitary.spectrum_subset_circle, cfcHom_apply_mem_elemental, Matrix.posSemidef_iff_isHermitian_and_spectrum_nonneg, spectrum.notMem_iff, isometry_cfcHom, CFC.spectrum_zero_eq, unitary.spectrum_subset_slitPlane_iff_norm_lt_two, Matrix.spectrum_toLin'
|