:: deftheorem defines Trace MATRIX_8:def 7 :
for n being Nat
for K being Field
for M being Matrix of n,K holds Trace M = Sum (diagonal_of_Matrix M);