Mathlib Changelog
v4
Changelog
About
Github
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_quasispectrum
View on Github ā