environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, MATRIX_1;
theorems BINOP_1, RLVECT_1, MATRIX_3, MATRIX_0, GROUP_1, FUNCT_1, FINSEQ_1, NAT_1, FINSEQ_2, TARSKI, FINSOP_1, FVSUM_1, SETWISEO, FUNCT_2, XBOOLE_0, GROUP_4, ENUMSET1, ZFMISC_1, FINSEQ_6, XREAL_1, FINSEQ_5, INTEGRA2, FUNCOP_1, FINSUB_1, XBOOLE_1, RELAT_1, SUBSET_1, RFINSEQ, FINSEQ_3, XXREAL_0, ORDINAL1, NAT_D, PARTFUN1, XREAL_0, CLASSES1, CARD_1, MATRIX_1;
schemes NAT_1, FUNCT_2, FINSEQ_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;
constructors HIDDEN, 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;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities XBOOLE_0, BINOP_1, FINSEQ_1, MATRIX_0, FINSEQ_2, GROUP_4, ALGSTR_0, RELAT_1;
expansions TARSKI, XBOOLE_0, FINSEQ_1, MATRIX_1;
Lm1:
<*1,2*> <> <*2,1*>
by FINSEQ_1:77;
theorem
for
K being
Field for
M being
Matrix of 2,
K holds
Det M = ((M * (1,1)) * (M * (2,2))) - ((M * (1,2)) * (M * (2,1)))
Lm2:
for n being Nat
for IT being Element of Permutations n st IT is even & n >= 1 holds
IT " is even