Theorem quasispectrum.of_subsingleton

Modification history

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