:: deftheorem Def3 defines diagonal ENTROPY1:def 3 :
for n being Nat
for MR being Matrix of n,REAL holds
( MR is diagonal iff for i, j being Nat st [i,j] in Indices MR & MR * (i,j) <> 0 holds
i = j );