environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, SUBSET_1, STRUCT_0, FUNCT_1, XBOOLE_0, ALGSTR_0, RELAT_1, PARTFUN1, ARYTM_3, CARD_3, ORDINAL4, PRELAMB, CLASSES1, XXREAL_0, TARSKI, CARD_1, SUPINF_2, ARYTM_1, NAT_1, FUNCT_2, FINSET_1, VALUED_1, RLSUB_1, ZFMISC_1, INT_1, ORDINAL1, RLVECT_2, ZMODUL01, ZMODUL03, ORDERS_1, RLVECT_3, RMOD_2, RANKNULL, MSAFREE2, INT_3, VECTSP_1, NEWTON, MONOID_0, VECTSP10, EC_PF_1, ZMODUL02, RLVECT_5, INT_2, MESFUNC1, MOD_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, BINOP_1, FUNCT_2, DOMAIN_1, FINSET_1, ORDERS_1, CARD_1, CLASSES1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, NAT_1, FINSEQ_1, FINSEQ_3, NEWTON, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, VECTSP_2, VECTSP_4, INT_2, VECTSP_6, VECTSP_9, MATRLIN, INT_3, BINOM, EC_PF_1, VECTSP_7, ZMODUL01, ZMODUL02;
definitions TARSKI, ZMODUL02, VECTSP_4, VECTSP_6, VECTSP_7, ZMODUL01;
theorems CARD_1, CARD_2, SUBSET_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCT_1, FUNCT_2, INT_1, NAT_1, RLSUB_2, RLVECT_1, TARSKI, ZMODUL01, RLVECT_2, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, ORDINAL1, STRUCT_0, PARTFUN1, FINSET_1, ORDERS_1, RFINSEQ, VECTSP_1, EC_PF_1, INT_2, WELLORD2, ZMODUL02, NAT_D, VECTSP_6, VECTSP_7, NUMBERS, VECTSP_4, VECTSP_9, MATRLIN, BINOM, RLVECT_3, MOD_3;
schemes FINSEQ_1, FUNCT_2, NAT_1, FUNCT_1, XFAMILY;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0, STRUCT_0, MEMBERED, FINSEQ_1, CARD_1, INT_1, XBOOLE_0, XXREAL_0, NAT_1, INT_3, RELAT_1, ALGSTR_1, VECTSP_1, ZMODUL02, ORDINAL1, VECTSP_7, ZMODUL01, VECTSP_2, MOD_3;
constructors HIDDEN, BINOP_2, BINOM, UPROOTS, RELSET_1, ORDERS_1, REALSET1, VECTSP_2, RLVECT_2, REAL_1, CLASSES1, FUNCT_7, NAT_D, GR_CY_1, EUCLID, VECTSP_6, VECTSP_9, VECTSP10, ALGSTR_1, ZMODUL01, ZMODUL02, BINOP_1, VECTSP_7, VECTSP_4, NEWTON;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0, ALGSTR_0, INT_3, VECTSP_1, BINOM, ZMODUL02, VECTSP_4, VECTSP_6, VECTSP_7;
expansions TARSKI, STRUCT_0, ZMODUL02, VECTSP_4, VECTSP_6, VECTSP_7, ZMODUL01, VECTSP_2;
Lm1:
for r being Element of INT.Ring
for n being Element of NAT
for i being Integer st i = n holds
i * r = n * r
Lm2:
for p being prime Element of INT.Ring
for V being Z_Module
for v, w being Vector of V st (ZMtoMQV (V,p,w)) /\ (ZMtoMQV (V,p,v)) <> {} holds
ZMtoMQV (V,p,w) = ZMtoMQV (V,p,v)
Lm3:
for p being Prime
for i being Element of INT holds i mod p is Element of (GF p)
Lm4:
for p being prime Element of INT.Ring
for V being free Z_Module
for i being Element of INT.Ring
for v being Element of V holds ZMtoMQV (V,p,((i mod p) * v)) = ZMtoMQV (V,p,(i * v))