Theorem quasispectrum.isCompact

Modification history

2026-08-23 19:23

Mathlib/Analysis/Normed/Algebra/Spectrum.lean

refactor: redefine `spectralRadius` in terms of `quasispectrum` (#42753)

Modified quasispectrum.isCompact View on Github →

2024-05-27 21:25

Mathlib/Analysis/NormedSpace/Spectrum.lean

feat: compactness of the quasispectrum (#13284)

Added quasispectrum.isCompact View on Github →