begin
:: deftheorem defines --> MATRIX_2:def 1 :
for n, m being Nat
for a being set holds n,m --> a = n |-> (m |-> a);
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 :
for a, b, c, d being set holds a,b ][ c,d = <*<*a,b*>,<*c,d*>*>;
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 :
for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is upper_triangular iff for i, j being Nat st [i,j] in Indices M & i > j holds
M * i,j = 0. K );
:: deftheorem defines lower_triangular MATRIX_2:def 4 :
for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is lower_triangular iff for i, j being Nat st [i,j] in Indices M & i < j holds
M * i,j = 0. K );
theorem
begin
theorem
canceled;
theorem
canceled;
theorem Th10:
Lm1:
for K being Field
for M being Matrix of K
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
K;
canceled;func DelCol M,
i -> Matrix of
K 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 K 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 K 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 :
for i being Nat
for K being Field
for M, b4 being Matrix of K holds
( b4 = DelCol M,i iff ( len b4 = len M & ( for k being Nat st k in dom M holds
b4 . k = Del (Line M,k),i ) ) );
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 :
for i, j, n being Nat
for K being Field
for M being Matrix of n,K holds Deleting M,i,j = DelCol (DelLine M,i),j;
begin
:: deftheorem Def9 defines permutational MATRIX_2:def 9 :
for IT being set holds
( IT is permutational iff ex n being Nat st
for x being set st x in IT holds
x is Permutation of (Seg n) );
:: deftheorem Def10 defines len MATRIX_2:def 10 :
for P being non empty permutational set
for b2 being Nat holds
( b2 = len P iff ex s being FinSequence st
( s in P & b2 = len s ) );
theorem
:: deftheorem Def11 defines Permutations MATRIX_2:def 11 :
for n being Nat
for b2 being set holds
( b2 = Permutations n iff for x being set holds
( x in b2 iff x is Permutation of (Seg n) ) );
theorem
theorem
theorem
canceled;
begin
:: deftheorem MATRIX_2:def 12 :
canceled;
:: deftheorem Def13 defines Group_of_Perm MATRIX_2:def 13 :
for n being Nat
for b2 being strict multMagma holds
( b2 = Group_of_Perm n iff ( the carrier of b2 = Permutations n & ( for q, p being Element of Permutations n holds the multF of b2 . q,p = p * q ) ) );
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
canceled;
theorem Th28:
:: deftheorem defines being_transposition MATRIX_2:def 14 :
for n being Nat
for p being Permutation of (Seg n) holds
( p is being_transposition iff ex i, j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) ) );
:: deftheorem Def15 defines even MATRIX_2:def 15 :
for n being Nat
for IT being Permutation of (Seg n) holds
( IT is even iff ex l being FinSequence of (Group_of_Perm n) st
( (len l) mod 2 = 0 & IT = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations n st
( l . i = q & q is being_transposition ) ) ) );
theorem
:: deftheorem defines - MATRIX_2:def 16 :
for K being Field
for n being Nat
for x being Element of K
for p being Element of Permutations n holds
( ( p is even implies - x,p = x ) & ( not p is even implies - x,p = - x ) );
:: deftheorem defines FinOmega MATRIX_2:def 17 :
for X being set st X is finite holds
FinOmega X = X;
theorem