Theorem SpectrumRestricts.spectralRadius_eq

Modification history

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