Commit 2026-10-17 11:31 6f48dc05
View on Github →feat(Analysis/Matrix/GelfandRadius): prove gelfandRadius (A * B) = gelfandRadius (B * A) for matrices (#44891)
This PR proves gelfandRadius (A * B) = gelfandRadius (B * A) for matrices. This is used in #42985 to compute the Gelfand radius of left-multiplication in a finite extension of a normed field.