Theorem IsometricContinuousFunctionalCalculus.spectrum_le

Modification history

2025-01-21 01:50
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
feat: show `IsGreatest (spectrum ℝ≥0 a) ‖a‖₊` for `IsometricContinuousFunctionalCalculus` (#20882) …
Added IsometricContinuousFunctionalCalculus.spectrum_leView on Github →