:: Determinant of Some Matrices of Field Elements
:: by Yatsuka Nakamura
::
:: Received January 4, 2006
:: Copyright (c) 2006-2021 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, FUNCT_2, FINSEQ_1, RELAT_1, FUNCT_1, TARSKI,
FINSEQ_2, XBOOLE_0, SUBSET_1, XXREAL_0, ARYTM_3, JORDAN3, ORDINAL4,
ARYTM_1, CARD_1, STRUCT_0, INT_1, CARD_3, GROUP_1, VECTSP_1, MATRIX_1,
MATRIX_3, ALGSTR_0, SETWISEO, FINSUB_1, BINOP_1, FINSOP_1, ABIAN,
TREES_1, SUPINF_2, FUNCOP_1, MESFUNC1, ZFMISC_1, QC_LANG1, PARTFUN1,
FINSEQ_5, CLASSES1, RFINSEQ, FUNCSDOM, MATRIX_7, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XXREAL_0, ORDINAL1, NAT_1,
NAT_D, RELAT_1, FUNCT_1, BINOP_1, ZFMISC_1, CARD_1, NUMBERS, VECTSP_1,
FUNCT_2, FUNCOP_1, SETWISEO, PARTFUN1, GROUP_4, FINSUB_1, NEWTON,
FINSOP_1, SETWOP_2, FINSEQ_1, FINSEQ_2, STRUCT_0, ALGSTR_0, MATRIX_1,
MATRIX_3, FINSEQ_6, MATRIX_0, CLASSES1, RFINSEQ, FINSEQ_5, GROUP_1;
constructors SETWISEO, REAL_1, NAT_1, NAT_D, FINSOP_1, NEWTON, RFINSEQ,
FINSEQ_5, ALGSTR_1, GROUP_4, MATRIX_3, FINSEQ_6, CLASSES1, RELSET_1,
BINOP_1, MATRIX_1;
registrations SUBSET_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2, FINSUB_1,
XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, GROUP_1, VECTSP_1,
MATRIX_1, FVSUM_1, FINSET_1, CARD_1, RELSET_1, FINSEQ_2, MATRIX_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
begin
reserve k,n,i,j for Nat;
theorem :: MATRIX_7:1
for f being Permutation of Seg 2 holds f=<*1,2*> or f=<*2,1*>;
theorem :: MATRIX_7:2
for f being FinSequence st f=<*1,2*> or f=<*2,1*> holds f is
Permutation of Seg 2;
theorem :: MATRIX_7:3
Permutations(2)={<*1,2*>,<*2,1*>};
theorem :: MATRIX_7:4
for p being Permutation of Seg 2 st p is being_transposition
holds p = <*2,1*>;
theorem :: MATRIX_7:5
for D being non empty set, f being FinSequence of D, k2 being
Nat st 1<=k2 & k2< len f holds f = mid(f,1,k2)^mid(f,k2+1,len f);
theorem :: MATRIX_7:6
for D being non empty set, f being FinSequence of D st 2<= len f
holds f = (f|(len f-'2))^mid(f,len f-'1,len f);
theorem :: MATRIX_7:7
for D being non empty set, f being FinSequence of D st 1<= len f
holds f = (f|(len f-'1))^mid(f,len f,len f);
theorem :: MATRIX_7:8
for a being Element of Group_of_Perm 2 st (ex q being Element of
Permutations 2 st q=a & q is being_transposition) holds a = <*2,1*>;
theorem :: MATRIX_7:9
for n being Nat,a,b being Element of Group_of_Perm n, pa,pb
being Element of Permutations n st a=pa & b=pb holds a*b=pb*pa;
theorem :: MATRIX_7:10
for a,b being Element of Group_of_Perm 2 st (ex p being Element
of Permutations 2 st p=a & p is being_transposition)& (ex q being Element of
Permutations 2 st q=b & q is being_transposition) holds a*b = <*1,2*>;
theorem :: MATRIX_7:11
for l being FinSequence of Group_of_Perm 2 st (len l) mod 2=0 &
(for i st i in dom l holds (ex q being Element of Permutations 2 st l.i=q & q
is being_transposition)) holds Product l = <*1,2*>;
theorem :: MATRIX_7:12
for K being Field, M being Matrix of 2,K holds Det M = (M*(1,1))*(M*(2
,2))-(M*(1,2))*(M*(2,1));
definition
let n be Nat,K be commutative Ring;
let M be (Matrix of n,K), a be Element of K;
redefine func a*M -> Matrix of n,K;
end;
theorem :: MATRIX_7:13
for K being Ring, n,m being Nat holds
len (0.(K,n,m))=n & dom (0.(K,n,m))=Seg n;
theorem :: MATRIX_7:14
for K being Ring, n being Nat, p being Element of
Permutations n, i being Nat st i in Seg n holds p.i in Seg n;
theorem :: MATRIX_7:15
for K being Ring, n being Nat st n>=1 holds Det (0.(K,n,n)
) = 0.K;
definition
let x be object; let y be set; let a,b be object;
func IFIN(x,y,a,b) -> object equals
:: MATRIX_7:def 1
a if x in y otherwise b;
end;
theorem :: MATRIX_7:16
for K being Ring, n being Nat st n>=1 holds Det (1.(K,n)) = 1_K;
definition
let n be Nat, K be Field, M be Matrix of n,K;
redefine attr M is diagonal means
:: MATRIX_7:def 2
for i,j being Nat st i
in Seg n & j in Seg n & i <> j holds M*(i,j) = 0.K;
end;
theorem :: MATRIX_7:17
for K being Field, n being Nat, A being Matrix of n,K st n
>=1 & A is diagonal holds Det A = (the multF of K) $$ (diagonal_of_Matrix A);
theorem :: MATRIX_7:18
for p being Element of Permutations(n) holds p" is Element of Permutations(n)
;
definition
let n;
let p be Element of Permutations(n);
redefine func p" -> Element of Permutations(n);
end;
::$CT
theorem :: MATRIX_7:20
for G being Group, f1,f2 being FinSequence of G
holds (Product (f1^f2))" = (Product f2)" * (Product f1)";
definition
let G be Group, f be FinSequence of G;
::$CD
func f" -> FinSequence of G means
:: MATRIX_7:def 4
len it = len f &
for i being Nat st i in dom f holds it/.i = (f/.i)";
end;
theorem :: MATRIX_7:21
for G being Group holds (<*>(the carrier of G))"=<*>(the carrier of G);
theorem :: MATRIX_7:22
for G being Group, f,g being FinSequence of G holds (f^g)"=(f")^ (g");
theorem :: MATRIX_7:23
for G being Group,a being Element of G holds (<*a*>)" =<* a" *>;
theorem :: MATRIX_7:24
for G being Group, f being FinSequence of G holds Product (f^( Rev f)")=1_G;
theorem :: MATRIX_7:25
for G being Group,f being FinSequence of G holds Product ((Rev f )" ^f)=1_G;
theorem :: MATRIX_7:26
for G being Group,f being FinSequence of G holds (Product f)" =
Product ((Rev f)");
theorem :: MATRIX_7:27
for ITP being Element of Permutations(n), ITG being Element of
Group_of_Perm(n) st ITG=ITP & n>=1 holds ITP"=ITG";
theorem :: MATRIX_7:28
for n being Nat, IT being Element of Permutations(n)
st n>=1 holds IT is even iff IT" is even;
theorem :: MATRIX_7:29
for n being Nat,K being commutative Ring, p being Element of
Permutations(n), x being Element of K st n>=1 holds -(x,p) = -(x,p");
theorem :: MATRIX_7:30
for K being commutative Ring,
f1,f2 being FinSequence of K holds (the multF
of K) $$ (f1^f2) = ((the multF of K)$$f1)*((the multF of K)$$f2);
theorem :: MATRIX_7:31
for K being commutative Ring,R1,R2 be FinSequence of K st R1,R2
are_fiberwise_equipotent holds (the multF of K)$$ R1 = (the multF of K)$$ R2;
theorem :: MATRIX_7:32
for n being Nat, K being commutative Ring, p being Element of
Permutations(n), f,g being FinSequence of K st len f=n & g=f*p holds f,g
are_fiberwise_equipotent;
theorem :: MATRIX_7:33
for n being Nat, K being commutative Ring, p being Element of
Permutations(n), f,g being FinSequence of K st n>=1 & len f=n & g=f*p holds (
the multF of K) $$ f = (the multF of K) $$ g;
theorem :: MATRIX_7:34
for n being Nat, K being Ring, p being Element of
Permutations(n), f being FinSequence of K st n>=1 & len f=n holds f*p is
FinSequence of K;
theorem :: MATRIX_7:35
for n being Nat, K being commutative Ring, p being Element of
Permutations(n), A being Matrix of n,K st n>=1 holds Path_matrix(p",A@) = (
Path_matrix(p,A))*p";
theorem :: MATRIX_7:36
for n being Nat, K being commutative Ring, p being Element of
Permutations(n), A being Matrix of n,K st n>=1 holds (Path_product(A@)).(p") =
(Path_product(A)).p;
theorem :: MATRIX_7:37
for n being Nat, K being commutative Ring, A being Matrix of n,K st n
>=1 holds Det (A) = Det (A@);