Theorem QuasispectrumRestricts.nnreal_of_nonneg

Modification history

2024-05-13 12:50
Mathlib/Analysis/NormedSpace/Spectrum.lean
refactor: generalize `SpectrumRestricts` to the `QuasispectrumRestricts`, preserving API (#12643)
Added QuasispectrumRestricts.nnreal_of_nonnegView on Github →