Theorem Matrix.spectralRadius_transpose

Modification history

2026-08-23 19:23
Mathlib/Analysis/Matrix/Spectrum.lean
refactor: redefine `spectralRadius` in terms of `quasispectrum` (#42753)
Modified Matrix.spectralRadius_transposeView on Github →
2026-08-13 15:55
Mathlib/Analysis/Matrix/Spectrum.lean
feat(Matrix): spectrum and spectral radius are invariant under transpose (#42627) …
Added Matrix.spectralRadius_transposeView on Github →