Theorem NonnegSpectrumClass.nonneg_of_mem_quasispectrum

Modification history

2025-08-21 02:05
Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean
feat(CStarAlgebra): `a => a ^ p` is operator monotone for `p ∈ Icc 0 1` (#27715) …
Added NonnegSpectrumClass.nonneg_of_mem_quasispectrumView on Github →