`BookProof.AbelianDiagonal.mem_commutant_of_diagonal` (e : n → ℂ) (d : n → ℂ) : Matrix.diagonal e * Matrix.diagonal d = Matrix.diagonal d * Matrix.diagonal e

Initializing...

`BookProof.AbelianDiagonal.mem_commutant_of_diagonal` (e : n → ℂ) (d : n → ℂ) : Matrix.diagonal e * Matrix.diagonal d = Matrix.diagonal d * Matrix.diagonal e · Prove2Me