:: On the Permanent of a Matrix
:: by Ewa Romanowicz and Adam Grabowski
::
:: Received January 4, 2006
:: Copyright (c) 2006 Association of Mizar Users
theorem Th1: :: MATRIX_9:1
Lm1:
<*1,2*> <> <*2,1*>
by GROUP_7:2;
Lm2:
<*2,1*> in Permutations 2
by MATRIX_7:3, TARSKI:def 2;
theorem Th2: :: MATRIX_9:2
theorem Th3: :: MATRIX_9:3
theorem Th4: :: MATRIX_9:4
theorem Th5: :: MATRIX_9:5
theorem Th6: :: MATRIX_9:6
:: deftheorem Def1 defines PPath_product MATRIX_9:def 1 :
:: deftheorem defines Per MATRIX_9:def 2 :
theorem :: MATRIX_9:7
theorem :: MATRIX_9:8
theorem Th9: :: MATRIX_9:9
theorem Th10: :: MATRIX_9:10
theorem Th11: :: MATRIX_9:11
theorem Th12: :: MATRIX_9:12
theorem :: MATRIX_9:13
theorem :: MATRIX_9:14
theorem Th15: :: MATRIX_9:15
theorem :: MATRIX_9:16
theorem Th17: :: MATRIX_9:17
theorem Th18: :: MATRIX_9:18
theorem Th19: :: MATRIX_9:19
Permutations 3
= {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>}
theorem Th20: :: MATRIX_9:20
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for
p being
Element of
Permutations 3 st
p = <*1,2,3*> holds
Path_matrix p,
M = <*a,e,i*>
theorem Th21: :: MATRIX_9:21
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for
p being
Element of
Permutations 3 st
p = <*3,2,1*> holds
Path_matrix p,
M = <*c,e,g*>
theorem Th22: :: MATRIX_9:22
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for
p being
Element of
Permutations 3 st
p = <*1,3,2*> holds
Path_matrix p,
M = <*a,f,h*>
theorem Th23: :: MATRIX_9:23
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for
p being
Element of
Permutations 3 st
p = <*2,3,1*> holds
Path_matrix p,
M = <*b,f,g*>
theorem Th24: :: MATRIX_9:24
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for
p being
Element of
Permutations 3 st
p = <*2,1,3*> holds
Path_matrix p,
M = <*b,d,i*>
theorem Th25: :: MATRIX_9:25
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
for
p being
Element of
Permutations 3 st
p = <*3,1,2*> holds
Path_matrix p,
M = <*c,d,h*>
theorem Th26: :: MATRIX_9:26
theorem Th27: :: MATRIX_9:27
(
<*1,3,2*> in Permutations 3 &
<*2,3,1*> in Permutations 3 &
<*2,1,3*> in Permutations 3 &
<*3,1,2*> in Permutations 3 &
<*1,2,3*> in Permutations 3 &
<*3,2,1*> in Permutations 3 )
Lm4:
( <*1,2,3*> <> <*3,2,1*> & <*1,2,3*> <> <*1,3,2*> & <*1,2,3*> <> <*2,3,1*> & <*1,2,3*> <> <*2,1,3*> & <*1,2,3*> <> <*3,1,2*> & <*3,2,1*> <> <*1,3,2*> & <*3,2,1*> <> <*2,3,1*> & <*3,2,1*> <> <*2,1,3*> & <*3,2,1*> <> <*3,1,2*> & <*1,3,2*> <> <*2,3,1*> & <*1,3,2*> <> <*2,1,3*> & <*1,3,2*> <> <*3,1,2*> & <*2,3,1*> <> <*2,1,3*> & <*2,3,1*> <> <*3,1,2*> & <*2,1,3*> <> <*3,1,2*> )
by GROUP_7:3;
theorem Th28: :: MATRIX_9:28
theorem :: MATRIX_9:29
theorem Th30: :: MATRIX_9:30
theorem Th31: :: MATRIX_9:31
theorem :: MATRIX_9:32
theorem Th33: :: MATRIX_9:33
theorem Th34: :: MATRIX_9:34
theorem Th35: :: MATRIX_9:35
theorem Th36: :: MATRIX_9:36
theorem Th37: :: MATRIX_9:37
(
<*2,1,3*> * <*1,3,2*> = <*2,3,1*> &
<*1,3,2*> * <*2,1,3*> = <*3,1,2*> &
<*2,1,3*> * <*3,2,1*> = <*3,1,2*> &
<*3,2,1*> * <*2,1,3*> = <*2,3,1*> &
<*3,2,1*> * <*3,2,1*> = <*1,2,3*> &
<*2,1,3*> * <*2,1,3*> = <*1,2,3*> &
<*1,3,2*> * <*1,3,2*> = <*1,2,3*> &
<*1,3,2*> * <*2,3,1*> = <*3,2,1*> &
<*2,3,1*> * <*2,3,1*> = <*3,1,2*> &
<*2,3,1*> * <*3,1,2*> = <*1,2,3*> &
<*3,1,2*> * <*2,3,1*> = <*1,2,3*> &
<*3,1,2*> * <*3,1,2*> = <*2,3,1*> &
<*1,3,2*> * <*3,2,1*> = <*2,3,1*> &
<*3,2,1*> * <*1,3,2*> = <*3,1,2*> )
theorem Th38: :: MATRIX_9:38
theorem Th39: :: MATRIX_9:39
Lm5:
<*1,2,3*> is even Permutation of Seg 3
by FINSEQ_2:62, MATRIX_2:29;
Lm6:
<*2,3,1*> is even Permutation of Seg 3
Lm7:
<*3,1,2*> is even Permutation of Seg 3
theorem :: MATRIX_9:40
Lm8:
for p being Permutation of Seg 3 holds p * <*1,2,3*> = p
Lm9:
for p being Permutation of Seg 3 holds <*1,2,3*> * p = p
theorem Th41: :: MATRIX_9:41
Lm10:
for l being FinSequence of (Group_of_Perm 3) st (len l) mod 2 = 0 & ( for i being Nat st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ) & not Product l = <*1,2,3*> & not Product l = <*2,3,1*> holds
Product l = <*3,1,2*>
theorem Th42: :: MATRIX_9:42
theorem Th43: :: MATRIX_9:43
theorem Th44: :: MATRIX_9:44
theorem :: MATRIX_9:45
theorem :: MATRIX_9:46
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = ((((((a * e) * i) - ((c * e) * g)) - ((a * f) * h)) + ((b * f) * g)) - ((b * d) * i)) + ((c * d) * h)
theorem :: MATRIX_9:47
for
K being
Field for
a,
b,
c,
d,
e,
f,
g,
h,
i being
Element of
K for
M being
Matrix of 3,
K st
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Per M = ((((((a * e) * i) + ((c * e) * g)) + ((a * f) * h)) + ((b * f) * g)) + ((b * d) * i)) + ((c * d) * h)
theorem Th48: :: MATRIX_9:48
theorem Th49: :: MATRIX_9:49
theorem Th50: :: MATRIX_9:50
theorem Th51: :: MATRIX_9:51
theorem Th52: :: MATRIX_9:52
Lm11:
for n being Nat
for K being Field
for M being Matrix of n,K st ex i being Element of NAT st
( i in Seg n & ( for k being Element of NAT st k in Seg n holds
(Col M,i) . k = 0. K ) ) holds
the addF of K $$ (FinOmega (Permutations n)),(PPath_product M) = 0. K
theorem :: MATRIX_9:53
theorem :: MATRIX_9:54
theorem :: MATRIX_9:55
theorem :: MATRIX_9:56