Theorem spectralRadius_eq_of_unital

Modification history

2026-08-23 19:23

Mathlib/Analysis/Normed/Algebra/Spectrum.lean

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

Added spectralRadius_eq_of_unital View on Github →