Theorem SpectrumRestricts.nnreal_le_iff

Modification history

2025-10-09 08:14
Mathlib/Analysis/Normed/Algebra/Spectrum.lean
chore: move some results from `Analysis/Normed/Algebra/Spectrum` to `Analysis/{Real, Complex}/Spectrum` (#29916)
Modified SpectrumRestricts.nnreal_le_iffView on Github →
2024-08-31 21:14
Mathlib/Analysis/Normed/Algebra/Spectrum.lean
feat: relate `∀ x ∈ spectrum ℝ≥0 a, x ≤ r` to the `ℝ`-spectrum (#16340)
Added SpectrumRestricts.nnreal_le_iffView on Github →