:: Some Properties Of Some Special Matrices :: by Xiaopeng Yue , Xiquan Liang and Zhongpin Sun :: :: Received December 7, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users
begin
definition
let n be Nat; let K be Field; let M1, M2 be Matrix of n,K;
for n being Nat for K being Field for M1, M2 being Matrix of n,K st n >0 holds ( M1 commutes_with M2 iff (M1 + M2)*(M1 + M2)=(((M1 * M1)+(M1 * M2))+(M1 * M2))+(M2 * M2) )