Theorem MonotoneOn.nnnorm_cfc

Modification history

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