Theorem NNReal.spectrum_nonempty

Modification history

2026-10-10 09:42
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
chore: delete deprecated declarations to March 2026 (#44240)
Deleted NNReal.spectrum_nonemptyView on Github →
2025-03-05 06:23
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
feat: generalize order typeclasses (#22569) …
Modified NNReal.spectrum_nonemptyView on Github →
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 NNReal.spectrum_nonemptyView on Github →