Theorem Matrix.gelfandRadius_mul_comm

Modification history

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