Theorem gelfandRadius_of_norm_nonpos

Modification history

2026-10-17 11:31
Mathlib/Analysis/Normed/Algebra/GelfandRadius.lean
feat(Analysis/Matrix/GelfandRadius): prove `gelfandRadius (A * B) = gelfandRadius (B * A)` for matrices (#44891) …
Added gelfandRadius_of_norm_nonposView on Github →