Commit 2024-05-13 12:50 7131ad07

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Algebra/Quasispectrum.lean

added theorem QuasispectrumRestricts.algebraMap_image

added theorem QuasispectrumRestricts.apply_mem

added theorem QuasispectrumRestricts.image

added theorem QuasispectrumRestricts.of_quasispectrum_eq

added theorem QuasispectrumRestricts.of_subset_range_algebraMap

added theorem QuasispectrumRestricts.subset_preimage

added structure QuasispectrumRestricts

added theorem SpectrumRestricts.algebraMap_image

added theorem SpectrumRestricts.apply_mem

added theorem SpectrumRestricts.image

added theorem SpectrumRestricts.of_rightInvOn

added theorem SpectrumRestricts.of_spectrum_eq

added theorem SpectrumRestricts.of_subset_range_algebraMap

added theorem SpectrumRestricts.rightInvOn

added theorem SpectrumRestricts.subset_preimage

added def SpectrumRestricts

added theorem mem_quasispectrum_iff

added theorem quasispectrum.algebraMap_mem_iff

added theorem quasispectrum.preimage_algebraMap

added theorem quasispectrumRestricts_iff

added theorem quasispectrumRestricts_iff_spectrumRestricts

added theorem quasispectrumRestricts_iff_spectrumRestricts_inr

added theorem spectrumRestricts_iff

Modified Mathlib/Algebra/Algebra/Spectrum.lean

deleted theorem SpectrumRestricts.algebraMap_image

deleted theorem SpectrumRestricts.apply_mem

deleted theorem SpectrumRestricts.image

deleted theorem SpectrumRestricts.of_spectrum_eq

deleted theorem SpectrumRestricts.of_subset_range_algebraMap

deleted theorem SpectrumRestricts.subset_preimage

deleted structure SpectrumRestricts

Modified Mathlib/Analysis/NormedSpace/Spectrum.lean

added theorem QuasispectrumRestricts.compactSpace

added theorem QuasispectrumRestricts.nnreal_iff

added theorem QuasispectrumRestricts.nnreal_of_nonneg

added theorem QuasispectrumRestricts.real_iff

Modified Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Instances.lean

Modified Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Restrict.lean

modified theorem SpectrumRestricts.compactSpace

modified def SpectrumRestricts.starAlgHom