Commit 2025-10-09 08:14 760bc88d

View on Github →

chore: move some results from Analysis/Normed/Algebra/Spectrum to Analysis/{Real, Complex}/Spectrum (#29916)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

Created Mathlib/Analysis/Complex/Spectrum.lean

added theorem QuasispectrumRestricts.real_iff

added theorem SpectrumRestricts.real_iff

Modified Mathlib/Analysis/Normed/Algebra/Spectrum.lean

deleted theorem QuasispectrumRestricts.le_nnreal_iff

deleted theorem QuasispectrumRestricts.lt_nnreal_iff

deleted theorem QuasispectrumRestricts.nnreal_iff

deleted theorem QuasispectrumRestricts.nnreal_of_nonneg

deleted theorem QuasispectrumRestricts.real_iff

deleted theorem SpectrumRestricts.le_nnreal_iff

deleted theorem SpectrumRestricts.lt_nnreal_iff

deleted theorem SpectrumRestricts.nnreal_iff

deleted theorem SpectrumRestricts.nnreal_le_iff

deleted theorem SpectrumRestricts.nnreal_lt_iff

deleted theorem SpectrumRestricts.nnreal_of_nonneg

deleted theorem SpectrumRestricts.real_iff

deleted theorem coe_mem_spectrum_real_of_nonneg

Created Mathlib/Analysis/Real/Spectrum.lean

added theorem QuasispectrumRestricts.le_nnreal_iff

added theorem QuasispectrumRestricts.lt_nnreal_iff

added theorem QuasispectrumRestricts.nnreal_iff

added theorem QuasispectrumRestricts.nnreal_of_nonneg

added theorem SpectrumRestricts.le_nnreal_iff

added theorem SpectrumRestricts.lt_nnreal_iff

added theorem SpectrumRestricts.nnreal_iff

added theorem SpectrumRestricts.nnreal_le_iff

added theorem SpectrumRestricts.nnreal_lt_iff

added theorem SpectrumRestricts.nnreal_of_nonneg

added theorem coe_mem_spectrum_real_of_nonneg