begin
:: deftheorem Def1 defines Idempotent MATRIX_8:def 1 :
:: deftheorem Def2 defines Nilpotent MATRIX_8:def 2 :
:: deftheorem Def3 defines Involutory MATRIX_8:def 3 :
:: deftheorem Def4 defines Self_Reversible MATRIX_8:def 4 :
theorem Th1:
theorem Th2:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th10:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th28:
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def5 defines is_similar_to MATRIX_8:def 5 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def6 defines is_congruent_Matrix_of MATRIX_8:def 6 :
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines Trace MATRIX_8:def 7 :
theorem
theorem Th54:
theorem
theorem Th56:
theorem Th57:
theorem
theorem
theorem Th60:
theorem
theorem
theorem