Theorem isQuasiregular_zero

Modification history

2026-08-23 19:23

Mathlib/Algebra/Algebra/Spectrum/Quasispectrum.lean

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

Modified isQuasiregular_zero View on Github →

2024-03-12 19:39

Mathlib/Algebra/Algebra/Quasispectrum.lean

feat: define `quasispectrum` for non-unital algebras (#11219) …

Added isQuasiregular_zero View on Github →