Theorem QuasispectrumRestricts.compactSpace

Modification history

2024-05-13 12:50

Mathlib/Analysis/NormedSpace/Spectrum.lean

refactor: generalize `SpectrumRestricts` to the `QuasispectrumRestricts`, preserving API (#12643)

Added QuasispectrumRestricts.compactSpace View on Github →