Theorem quasispectrum.zero_eq_nonunits

Modification history

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