Theorem ContinuousLinearMap.IsPositive.spectrumRestricts

Modification history

2024-09-04 22:22
Mathlib/Analysis/InnerProductSpace/StarOrder.lean
feat: `H →L[ℂ] H` is a `StarOrderedRing` when `H` is a Hilbert space (#16462)
Added ContinuousLinearMap.IsPositive.spectrumRestrictsView on Github →