Theorem SpectrumRestricts.nnreal_iff_spectralRadius_le

Modification history

2024-02-22 19:15
Mathlib/Analysis/NormedSpace/Spectrum.lean
feat: simpler conditions for SpectrumRestricts for `ℂ`, `ℝ` and `ℝ≥0`. (#10826) …
Added SpectrumRestricts.nnreal_iff_spectralRadius_leView on Github →