begin
:: deftheorem Def1 defines commutes_with MATRIX_6:def 1 :
:: deftheorem Def2 defines is_reverse_of MATRIX_6:def 2 :
:: deftheorem Def3 defines invertible MATRIX_6:def 3 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem
theorem
theorem Th6:
theorem Th7:
:: deftheorem Def4 defines ~ MATRIX_6:def 4 :
theorem Th8:
theorem
theorem Th10:
theorem
theorem
theorem
theorem
theorem
theorem Th16:
theorem
theorem
theorem
:: deftheorem Def5 defines symmetric MATRIX_6:def 5 :
theorem
canceled;
theorem Th21:
theorem
theorem
theorem Th24:
for
n being
Nat for
K being
Field for
M1,
M2 being
Matrix of
n,
K holds
(M1 + M2) @ = (M1 @ ) + (M2 @ )
theorem
theorem
theorem Th27:
theorem
theorem
:: deftheorem Def6 defines antisymmetric MATRIX_6:def 6 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th37:
theorem
theorem
theorem
theorem Th41:
:: deftheorem Def7 defines Orthogonal MATRIX_6:def 7 :
theorem Th42:
theorem Th43:
theorem
theorem
theorem Th46:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem Th58:
theorem
theorem
theorem