:: Determinant of Some Matrices of Field Elements
:: by Yatsuka Nakamura
::
:: Received January 4, 2006
:: Copyright (c) 2006 Association of Mizar Users
theorem Th1: :: MATRIX_7:1
theorem Th2: :: MATRIX_7:2
theorem Th3: :: MATRIX_7:3
theorem Th4: :: MATRIX_7:4
theorem Th5: :: MATRIX_7:5
theorem Th6: :: MATRIX_7:6
theorem Th7: :: MATRIX_7:7
Lm1:
<*1,2*> <> <*2,1*>
by GROUP_7:2;
theorem Th8: :: MATRIX_7:8
theorem :: MATRIX_7:9
theorem Th10: :: MATRIX_7:10
theorem Th11: :: MATRIX_7:11
theorem :: MATRIX_7:12
theorem Th13: :: MATRIX_7:13
theorem Th14: :: MATRIX_7:14
theorem :: MATRIX_7:15
:: deftheorem Def1 defines IFIN MATRIX_7:def 1 :
for
x,
y,
a,
b being
set holds
( (
x in y implies
IFIN x,
y,
a,
b = a ) & ( not
x in y implies
IFIN x,
y,
a,
b = b ) );
theorem :: MATRIX_7:16
:: deftheorem Def2 defines diagonal MATRIX_7:def 2 :
theorem :: MATRIX_7:17
theorem Th18: :: MATRIX_7:18
theorem Th19: :: MATRIX_7:19
:: deftheorem defines @ MATRIX_7:def 3 :
theorem :: MATRIX_7:20
:: deftheorem Def4 defines " MATRIX_7:def 4 :
theorem Th21: :: MATRIX_7:21
theorem Th22: :: MATRIX_7:22
theorem Th23: :: MATRIX_7:23
theorem Th24: :: MATRIX_7:24
theorem Th25: :: MATRIX_7:25
theorem Th26: :: MATRIX_7:26
theorem Th27: :: MATRIX_7:27
Lm2:
for n being Element of NAT
for IT being Element of Permutations n st IT is even & n >= 1 holds
IT " is even
theorem Th28: :: MATRIX_7:28
theorem Th29: :: MATRIX_7:29
theorem Th30: :: MATRIX_7:30
theorem Th31: :: MATRIX_7:31
theorem Th32: :: MATRIX_7:32
theorem :: MATRIX_7:33
theorem Th34: :: MATRIX_7:34
theorem Th35: :: MATRIX_7:35
theorem Th36: :: MATRIX_7:36
theorem :: MATRIX_7:37