Theorem SpectrumRestricts.compactSpace

Modification history

2024-05-13 12:50
Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Restrict.lean
refactor: generalize `SpectrumRestricts` to the `QuasispectrumRestricts`, preserving API (#12643)
Modified SpectrumRestricts.compactSpaceView on Github →
2024-03-07 08:49
Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Restrict.lean
feat: restriction of the continuous functional calculus to a scalar subring (#10768)
Added SpectrumRestricts.compactSpaceView on Github →