environ
vocabularies HIDDEN, GAUSSINT, NUMBERS, SUBSET_1, RLVECT_1, STRUCT_0, PBOOLE, FUNCT_4, FUNCT_1, RAT_1, XBOOLE_0, ALGSTR_0, RELAT_1, ARYTM_3, CARD_3, BINOM, RLSUB_2, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, MSSUBFAM, ARYTM_1, NAT_1, FUNCT_2, FINSET_1, FUNCOP_1, RLSUB_1, ZFMISC_1, INT_1, RLVECT_2, ZMODUL01, ZMODUL03, RLVECT_3, RMOD_2, RANKNULL, MSAFREE2, INT_3, COMPLEX1, INT_2, VECTSP_1, MESFUNC1, XCMPLX_0, REALSET1, MONOID_0, ZMODUL02, RLVECT_5, ZMODUL04, ZMODUL05, ZMODUL06, MOD_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, RAT_1, INT_2, REALSET1, FUNCT_4, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6, INT_3, VECTSP_7, VECTSP_9, MATRLIN, BINOM, ZMODUL01, ZMODUL02, ZMODUL03, GAUSSINT, MOD_2, ZMODUL04, ZMODUL05;
definitions VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, ZMODUL01;
theorems CARD_1, CARD_2, SUBSET_1, FUNCT_1, FUNCT_2, INT_1, NAT_1, RLVECT_1, TARSKI, ZMODUL01, BINOP_2, ZFMISC_1, RELAT_1, GAUSSINT, ZMODUL03, XBOOLE_0, XBOOLE_1, XXREAL_0, STRUCT_0, XCMPLX_0, VECTSP_1, EULER_1, INT_2, ZMODUL02, NAT_D, VECTSP_6, VECTSP_7, VECTSP_4, VECTSP_5, VECTSP_9, BINOM, ABSVALUE, ZMODUL04, ZMODUL05, MOD_2;
schemes FUNCT_2, NAT_1;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0, STRUCT_0, RLVECT_1, MEMBERED, CARD_1, INT_1, XBOOLE_0, ORDINAL1, XXREAL_0, NAT_1, INT_3, RELAT_1, ZMODUL02, GAUSSINT, VECTSP_9, FUNCT_4, RAT_1, XCMPLX_0, ZMODUL03, ZMODUL04, ZMODUL05, VECTSP_4, VECTSP_5, MOD_2, VECTSP_2, VECTSP_7;
constructors HIDDEN, BINOP_2, BINOM, UPROOTS, RELSET_1, ORDERS_1, REALSET1, FUNCT_4, VECTSP_6, VECTSP_9, VECTSP10, ALGSTR_1, ZMODUL04, ZMODUL05, INT_2, ZMODUL01, ZMODUL02, MATRLIN, MOD_2, INT_3;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XCMPLX_0, STRUCT_0, ALGSTR_0, INT_3, GAUSSINT, ZMODUL02, SUBSET_1, RLVECT_2, VECTSP_2, VECTSP_4, VECTSP_6, VECTSP_7;
expansions TARSKI, STRUCT_0, ZMODUL03, ZMODUL05, VECTSP_2, VECTSP_4, VECTSP_5, ZMODUL01, VECTSP_6, VECTSP_7;
ThTV1:
for V being Z_Module holds 0. V is torsion
ThTZM:
for V being Z_Module holds (0). V is torsion
ThLin4:
for V being Z_Module
for A being Subset of V holds A is Subset of (Lin A)
ThLin7:
for V being Z_Module
for A being linearly-independent Subset of V holds A is Basis of (Lin A)
LmGCD1:
for i1, i2 being Integer st i1,i2 are_coprime holds
ex j1, j2 being Element of INT.Ring st (i1 * j1) + (i2 * j2) = 1
LmGCD:
for i1, i2 being Element of INT.Ring st i1,i2 are_coprime holds
ex j1, j2 being Element of INT.Ring st (i1 * j1) + (i2 * j2) = 1
HM4:
for X, Y being Z_Module
for A being Subset of X
for L being linear-transformation of X,Y st L is bijective & A is linearly-independent holds
L .: A is linearly-independent
HM9:
for X, Y being Z_Module
for T being linear-transformation of X,Y st T is bijective & X is free holds
Y is free
HM11:
for X, Y being free Z_Module
for T being linear-transformation of X,Y
for A being Subset of X st T is bijective & A is Basis of X holds
T .: A is Basis of Y
HM13:
for X, Y being free Z_Module
for T being linear-transformation of X,Y st T is bijective & X is finite-rank holds
Y is finite-rank