Theorem SpectrumRestricts.real_iff

Modification history

2025-10-09 08:14
Mathlib/Analysis/Complex/Spectrum.lean
chore: move some results from `Analysis/Normed/Algebra/Spectrum` to `Analysis/{Real, Complex}/Spectrum` (#29916)
Modified SpectrumRestricts.real_iffView on Github →
2024-02-22 19:15
Mathlib/Analysis/NormedSpace/Spectrum.lean
feat: simpler conditions for SpectrumRestricts for `ℂ`, `ℝ` and `ℝ≥0`. (#10826) …
Added SpectrumRestricts.real_iffView on Github →