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