Theorem exists_nnnorm_quasispectrum_eq_spectralRadius

Modification history

2026-08-23 19:23
Mathlib/Analysis/Normed/Algebra/Spectrum.lean
refactor: redefine `spectralRadius` in terms of `quasispectrum` (#42753)
Added exists_nnnorm_quasispectrum_eq_spectralRadiusView on Github →