:: Transpose Matrices and Groups of Permutations
:: by Katarzyna Jankowska
::
:: Received May 20, 1992
:: Copyright (c) 1992 Association of Mizar Users
:: deftheorem defines --> MATRIX_2:def 1 :
theorem Th1: :: MATRIX_2:1
theorem :: MATRIX_2:2
definition
let a,
b,
c,
d be
set ;
func a,
b ][ c,
d -> tabular FinSequence equals :: MATRIX_2:def 2
<*<*a,b*>,<*c,d*>*>;
correctness
coherence
<*<*a,b*>,<*c,d*>*> is tabular FinSequence;
end;
:: deftheorem defines ][ MATRIX_2:def 2 :
theorem Th3: :: MATRIX_2:3
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: :: MATRIX_2:4
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 :: MATRIX_2:5
theorem :: MATRIX_2:6
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 :: MATRIX_2:7
theorem :: MATRIX_2:8
canceled;
theorem :: MATRIX_2:9
canceled;
theorem Th10: :: MATRIX_2:10
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 :: MATRIX_2:def 6
(
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 :
theorem Th11: :: MATRIX_2:11
theorem Th12: :: MATRIX_2:12
theorem :: MATRIX_2:13
theorem :: MATRIX_2:14
theorem Th15: :: MATRIX_2:15
theorem Th16: :: MATRIX_2:16
theorem :: MATRIX_2:17
theorem :: MATRIX_2:18
:: deftheorem MATRIX_2:def 7 :
canceled;
:: deftheorem defines Deleting MATRIX_2:def 8 :
:: deftheorem Def9 defines permutational MATRIX_2:def 9 :
:: deftheorem Def10 defines len MATRIX_2:def 10 :
theorem :: MATRIX_2:19
:: deftheorem Def11 defines Permutations MATRIX_2:def 11 :
theorem :: MATRIX_2:20
theorem :: MATRIX_2:21
theorem :: MATRIX_2:22
canceled;
:: deftheorem MATRIX_2:def 12 :
canceled;
:: deftheorem Def13 defines Group_of_Perm MATRIX_2:def 13 :
theorem Th23: :: MATRIX_2:23
theorem Th24: :: MATRIX_2:24
theorem Th25: :: MATRIX_2:25
theorem Th26: :: MATRIX_2:26
theorem :: MATRIX_2:27
canceled;
theorem Th28: :: MATRIX_2:28
:: deftheorem defines being_transposition MATRIX_2:def 14 :
:: deftheorem Def15 defines even MATRIX_2:def 15 :
theorem :: MATRIX_2:29
:: deftheorem defines - MATRIX_2:def 16 :
:: deftheorem defines FinOmega MATRIX_2:def 17 :
theorem :: MATRIX_2:30