:: deftheorem defines diagonal MATRIX_7:def 2 :
for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is diagonal iff for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
M * (i,j) = 0. K );