Theorem quasispectrumRestricts_iff_spectrumRestricts_inr

Modification history

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