:: On the Permanent of a Matrix
:: by Ewa Romanowicz and Adam Grabowski
::
:: Received January 4, 2006
:: Copyright (c) 2006-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, VECTSP_1, FINSUB_1, TARSKI, XBOOLE_0, SUBSET_1,
FINSEQ_2, FINSET_1, FINSEQ_1, FUNCT_1, RELAT_1, FINSEQ_5, FUNCT_2,
CARD_1, MATRIX_1, STRUCT_0, ALGSTR_0, SETWISEO, MATRIX_3, CALCUL_2,
XXREAL_0, SUPINF_2, FUNCOP_1, BINOP_1, ARYTM_3, ORDINAL4, TREES_1,
ZFMISC_1, ARYTM_1, CARD_3, ABIAN, INT_1, PARTFUN1, GROUP_1, FUNCT_7,
MATRIX_9;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, NAT_D, ENUMSET1, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
FINSEQ_1, FUNCOP_1, FINSEQ_2, BINOP_1, STRUCT_0, ALGSTR_0, GROUP_1,
VECTSP_1, SETWISEO, GROUP_4, SETWOP_2, FINSUB_1, MATRIX_0, FINSEQ_4,
FINSEQ_5, MATRIX_1, MATRIX_3, XXREAL_0;
constructors BINOP_1, SETWISEO, NAT_1, NAT_D, FINSEQ_4, FINSOP_1, FINSEQ_5,
ALGSTR_1, GROUP_4, MATRIX_7, RELSET_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2,
FINSET_1, FINSUB_1, XXREAL_0, XREAL_0, FINSEQ_1, FINSEQ_5, FINSEQ_6,
STRUCT_0, GROUP_1, VECTSP_1, MATRIX_1, FVSUM_1, RELSET_1, FINSEQ_2,
CARD_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
reserve x for set,
i,j,k,n for Nat,
K for Field;
theorem :: MATRIX_9:1
for a, A being set st a in A holds {a} in Fin A;
registration
let n be Nat;
cluster non empty for Element of Fin Permutations n;
end;
scheme :: MATRIX_9:sch 1
NonEmptyFiniteX { n() -> Element of NAT, A() -> non empty Element of Fin
Permutations n(), P[set] } : P[A()]
provided
for x being Element of Permutations n() st x in A() holds P[{x}] and
for x being Element of Permutations n(), B being non empty Element
of Fin Permutations n() st x in A() & B c= A() & not x in B & P[B] holds P[B \/
{x}];
registration
let n;
cluster one-to-one FinSequence-like for Function of Seg n, Seg n;
end;
registration
let n;
cluster id Seg n -> FinSequence-like;
end;
theorem :: MATRIX_9:2
(Rev idseq 2).1 = 2 & (Rev idseq 2).2 = 1;
theorem :: MATRIX_9:3
for f being one-to-one Function st dom f = Seg 2 & rng f = Seg 2
holds f = id Seg 2 or f = Rev id Seg 2;
begin :: Permutations
theorem :: MATRIX_9:4
Rev idseq n in Permutations n;
theorem :: MATRIX_9:5
for f being FinSequence st n <> 0 & f in Permutations n holds Rev
f in Permutations n;
theorem :: MATRIX_9:6
Permutations 2 = { idseq 2, Rev idseq 2 };
begin :: The Permanent of a Matrix
definition
let n,K;
let M be Matrix of n,K;
func PPath_product M -> Function of Permutations n, the carrier of K means
:: MATRIX_9:def 1
for p being Element of Permutations(n) holds it.p = (the multF of K) $$
Path_matrix(p,M);
end;
definition
let n, K;
let M be Matrix of n,K;
func Per M -> Element of K equals
:: MATRIX_9:def 2
(the addF of K) $$ (In (Permutations n, Fin Permutations n),
PPath_product M);
end;
reserve a,b,c,d for Element of K;
theorem :: MATRIX_9:7
Per <*<*a*>*> = a;
theorem :: MATRIX_9:8
for K being Field, n being Element of NAT st n >= 1 holds Per (0.(K,n,
n)) = 0.K;
theorem :: MATRIX_9:9
for p being Element of Permutations 2 st p = idseq 2 holds
Path_matrix (p, (a,b)][(c,d)) = <* a,d *>;
theorem :: MATRIX_9:10
for p being Element of Permutations 2 st p = Rev idseq 2 holds
Path_matrix (p, (a,b)][(c,d)) = <* b,c *>;
theorem :: MATRIX_9:11
(the multF of K) $$ <* a,b *> = a * b;
begin
registration
cluster odd for Permutation of Seg 2;
end;
registration
let n be Nat;
cluster even for Permutation of Seg n;
end;
theorem :: MATRIX_9:12
<*2,1*> is odd Permutation of Seg 2;
theorem :: MATRIX_9:13
Det (a,b)][(c,d) = a * d - b * c;
theorem :: MATRIX_9:14
Per (a,b)][(c,d) = a * d + b * c;
theorem :: MATRIX_9:15
Rev idseq 3 = <*3,2,1*>;
reserve D for non empty set;
theorem :: MATRIX_9:16
for x,y,z being Element of D for f being FinSequence of D st f = <*x,y
,z*> holds Rev f = <*z,y,x*>;
theorem :: MATRIX_9:17
for f, g being FinSequence st f ^ g in Permutations n holds f ^
Rev g in Permutations n;
theorem :: MATRIX_9:18
for f, g being FinSequence st f ^ g in Permutations n holds g ^
f in Permutations n;
theorem :: MATRIX_9:19
Permutations 3 = {<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,
3*>,<*3,1,2*>};
theorem :: MATRIX_9:20
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*>*> for p being Element of Permutations
3 st p = <*1,2,3*> holds Path_matrix (p,M) = <* a,e,i *>;
theorem :: MATRIX_9:21
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*>*> for p being Element of Permutations
3 st p = <*3,2,1*> holds Path_matrix (p,M) = <* c,e,g *>;
theorem :: MATRIX_9:22
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*>*> for p being Element of Permutations
3 st p = <*1,3,2*> holds Path_matrix (p,M) = <* a,f,h *>;
theorem :: MATRIX_9:23
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*>*> for p being Element of Permutations
3 st p = <*2,3,1*> holds Path_matrix (p,M) = <* b,f,g *>;
theorem :: MATRIX_9:24
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*>*> for p being Element of Permutations
3 st p = <*2,1,3*> holds Path_matrix (p,M) = <* b,d,i *>;
theorem :: MATRIX_9:25
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*>*> for p being Element of Permutations
3 st p = <*3,1,2*> holds Path_matrix (p,M) = <* c,d,h *>;
theorem :: MATRIX_9:26
(the multF of K) $$ <* a,b,c *> = a * b * c;
theorem :: 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;
theorem :: MATRIX_9:28
<*2,3,1*>" = <*3,1,2*>;
theorem :: MATRIX_9:29
for a being Element of Group_of_Perm 3 st a = <*2,3,1*> holds a" = <*3 ,1,2*>
;
begin :: Transpositions
theorem :: MATRIX_9:30
for p being Permutation of Seg 3 st p = <* 1,3,2 *> holds p is
being_transposition;
theorem :: MATRIX_9:31
for p being Permutation of Seg 3 st p = <* 2,1,3 *> holds p is
being_transposition;
theorem :: MATRIX_9:32
for p being Permutation of Seg 3 st p = <* 3,2,1 *> holds p is
being_transposition;
theorem :: MATRIX_9:33
for p being Permutation of Seg n st p = id Seg n holds not p is
being_transposition;
theorem :: MATRIX_9:34
for p being Permutation of Seg 3 st p = <* 3,1,2 *> holds not p
is being_transposition;
theorem :: MATRIX_9:35
for p being Permutation of Seg 3 st p = <* 2,3,1 *> holds not p
is being_transposition;
begin :: Corrollaries
theorem :: MATRIX_9:36
for f being Permutation of Seg n holds f is FinSequence of Seg n;
theorem :: 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 :: MATRIX_9:38
for p being Permutation of Seg 3 st p is being_transposition
holds p = <*2,1,3*> or p = <*1,3,2*> or p = <*3,2,1*>;
theorem :: MATRIX_9:39
for f, g being Element of Permutations n holds f * g in Permutations n;
theorem :: MATRIX_9:40
for l being FinSequence of Group_of_Perm n st (len l) mod 2 = 0 & (for
i being Element of NAT st i in dom l ex q being Element of Permutations n st l.
i = q & q is being_transposition) holds Product l is even Permutation of Seg n;
theorem :: MATRIX_9:41
for l being FinSequence of Group_of_Perm 3 st (len l) mod 2 = 0
& (for i being Element of NAT st i in dom l ex q being Element of Permutations
3 st l.i = q & q is being_transposition) holds Product l = <*1,2,3*> or Product
l = <*2,3,1*> or Product l = <*3,1,2*>;
registration
cluster odd for Permutation of Seg 3;
end;
theorem :: MATRIX_9:42
<*3,2,1*> is odd Permutation of Seg 3;
theorem :: MATRIX_9:43
<*2,1,3*> is odd Permutation of Seg 3;
theorem :: MATRIX_9:44
<*1,3,2*> is odd Permutation of Seg 3;
theorem :: MATRIX_9:45
for p being odd Permutation of Seg 3 holds p = <*3,2,1*> or p = <*1,3,
2*> or p = <*2,1,3*>;
begin :: Determinant and Permanent
theorem :: MATRIX_9:46
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 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 :: MATRIX_9:48
for i,n being Element of NAT for p being Element of Permutations
n st i in Seg n holds ex k being Element of NAT st k in Seg n & i = p.k;
theorem :: MATRIX_9:49
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
for p being Element of Permutations n holds ex l being Element of NAT st l in
Seg n & Path_matrix (p,M).l = 0.K;
theorem :: MATRIX_9:50
for p being Element of Permutations n 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 (Path_product M).p = 0.K;
theorem :: MATRIX_9:51
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) $$ (In(Permutations n,Fin Permutations n), Path_product M)
= 0.K;
theorem :: MATRIX_9:52
for p being Element of Permutations n 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 (PPath_product M).p = 0.K;
theorem :: MATRIX_9:53
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 Det M
= 0.K;
theorem :: MATRIX_9:54
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 Per M
= 0.K;
begin :: Auxiliary Lemmas for Further Work
theorem :: MATRIX_9:55
for M,N being Matrix of n, K st i in Seg n for p being Element of
Permutations n holds ex k being Element of NAT st k in Seg n & i = p.k & Col(N,
i)/.k = Path_matrix (p, N)/.k;
theorem :: MATRIX_9:56
for a being Element of K for M,N 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 = a * Col(N,i)/.k) & (for l being Element of NAT st l <> i & l in
Seg n holds Col(M,l) = Col(N,l))) for p being Element of Permutations n holds
ex l being Element of NAT st l in Seg n & Path_matrix (p,M)/.l = a * (
Path_matrix (p,N)/.l);