Theorem CStarAlgebra.le_nnnorm_of_mem_quasispectrum

Modification history

2024-10-30 16:54
Mathlib/Analysis/CStarAlgebra/Spectrum.lean
feat: positive contractions in a Cā‹†-algebra form a directed set (#18016)
Added CStarAlgebra.le_nnnorm_of_mem_quasispectrumView on Github ā†’