theorem Th56: :: MATRIX_8:56

for n being Nat
for K being Field
for M1 being Matrix of n,K holds Trace (- M1) = - (Trace M1)