Golfand radius of matrices

This file proves some results on the Gelfand radius of matrices with respect to the operator norm.

theorem Matrix.gelfandRadius_mul_comm {R : Type u_1} {m : Type u_2} {n : Type u_3} [SeminormedCommRing R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m n R) (B : Matrix n m R) : gelfandRadius (A * B) = gelfandRadius (B * A)

theorem Matrix.gelfandRadius_blockDiagonal {R : Type u_1} {m : Type u_2} {n : Type u_3} [SeminormedCommRing R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (M : n → Matrix m m R) : gelfandRadius (blockDiagonal M) = ⨆ (i : n), gelfandRadius (M i)