Theorem SpectrumRestricts.of_spectrum_eq

Modification history

2024-05-13 12:50
Mathlib/Algebra/Algebra/Quasispectrum.lean
refactor: generalize `SpectrumRestricts` to the `QuasispectrumRestricts`, preserving API (#12643)
Modified SpectrumRestricts.of_spectrum_eqView on Github →
2024-02-21 19:00
Mathlib/Algebra/Algebra/Spectrum.lean
feat: add a `SpectrumRestricts` structure (#10735) …
Added SpectrumRestricts.of_spectrum_eqView on Github →