Theorem IsSelfAdjoint.spectrum_nonempty

Modification history

2024-08-31 14:29
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
feat: any element satisfying the predicate of a continuous functional calculus has nonempty spectrum (#16343) …
Added IsSelfAdjoint.spectrum_nonemptyView on Github →