begin
:: deftheorem defines --> MATRIX_2:def 1 :
theorem Th1:
theorem
definition
let a,
b,
c,
d be
set ;
func a,
b ][ c,
d -> tabular FinSequence equals
<*<*a,b*>,<*c,d*>*>;
correctness
coherence
<*<*a,b*>,<*c,d*>*> is tabular FinSequence;
end;
:: deftheorem defines ][ MATRIX_2:def 2 :
theorem Th3:
for
x1,
x2,
y1,
y2 being
set holds
(
len (x1,x2 ][ y1,y2) = 2 &
width (x1,x2 ][ y1,y2) = 2 &
Indices (x1,x2 ][ y1,y2) = [:(Seg 2),(Seg 2):] )
theorem Th4:
for
x1,
x2,
y1,
y2 being
set holds
(
[1,1] in Indices (x1,x2 ][ y1,y2) &
[1,2] in Indices (x1,x2 ][ y1,y2) &
[2,1] in Indices (x1,x2 ][ y1,y2) &
[2,2] in Indices (x1,x2 ][ y1,y2) )
theorem
theorem
for
D being non
empty set for
a,
b,
c,
d being
Element of
D holds
(
(a,b ][ c,d) * 1,1
= a &
(a,b ][ c,d) * 1,2
= b &
(a,b ][ c,d) * 2,1
= c &
(a,b ][ c,d) * 2,2
= d )
:: deftheorem Def3 defines upper_triangular MATRIX_2:def 3 :
:: deftheorem defines lower_triangular MATRIX_2:def 4 :
theorem
begin
theorem
canceled;
theorem
canceled;
theorem Th10:
Lm1:
for K being Field
for M being Matrix of
for k being Nat st k in dom M holds
M . k = Line M,k
definition
let i be
Nat;
let K be
Field;
let M be
Matrix of ;
canceled;func DelCol M,
i -> Matrix of
means
(
len it = len M & ( for
k being
Nat st
k in dom M holds
it . k = Del (Line M,k),
i ) );
existence
ex b1 being Matrix of st
( len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del (Line M,k),i ) )
uniqueness
for b1, b2 being Matrix of st len b1 = len M & ( for k being Nat st k in dom M holds
b1 . k = Del (Line M,k),i ) & len b2 = len M & ( for k being Nat st k in dom M holds
b2 . k = Del (Line M,k),i ) holds
b1 = b2
end;
:: deftheorem MATRIX_2:def 5 :
canceled;
:: deftheorem defines DelCol MATRIX_2:def 6 :
theorem Th11:
theorem Th12:
theorem
theorem
theorem Th15:
theorem Th16:
theorem
theorem
:: deftheorem MATRIX_2:def 7 :
canceled;
:: deftheorem defines Deleting MATRIX_2:def 8 :
begin
:: deftheorem Def9 defines permutational MATRIX_2:def 9 :
:: deftheorem Def10 defines len MATRIX_2:def 10 :
theorem
:: deftheorem Def11 defines Permutations MATRIX_2:def 11 :
theorem
theorem
theorem
canceled;
begin
:: deftheorem MATRIX_2:def 12 :
canceled;
:: deftheorem Def13 defines Group_of_Perm MATRIX_2:def 13 :
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
canceled;
theorem Th28:
:: deftheorem defines being_transposition MATRIX_2:def 14 :
:: deftheorem Def15 defines even MATRIX_2:def 15 :
theorem
:: deftheorem defines - MATRIX_2:def 16 :
:: deftheorem defines FinOmega MATRIX_2:def 17 :
theorem