environ
vocabularies HIDDEN, GAUSSINT, NUMBERS, FINSEQ_1, SUBSET_1, RLVECT_1, STRUCT_0, FUNCT_1, RAT_1, XBOOLE_0, ALGSTR_0, RELAT_1, PARTFUN1, ARYTM_3, CARD_3, ORDINAL4, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, MSSUBFAM, ARYTM_1, NAT_1, FINSET_1, FUNCOP_1, RLSUB_1, QC_LANG1, BINOP_1, ZFMISC_1, INT_1, ZMODUL01, ZMODUL03, FINSEQ_4, RLVECT_3, RMOD_2, RANKNULL, UNIALG_1, FUNCT_7, GROUP_1, INT_3, COMPLEX1, VECTSP_1, MESFUNC1, XCMPLX_0, REALSET1, MATRLIN, ZMODUL02, RLVECT_5, ZMODUL06, NORMSP_1, BHSP_1, ABIAN, RVSUM_1, MATRIX_1, MATRIX_3, MOD_3, ZMATRLIN, FUNCT_5, ZMODLAT1, TREES_1, MFOLD_2, BILINEAR, HAHNBAN, FVSUM_1, INCSP_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, REALSET1, FINSET_1, CARD_1, FUNCT_5, XCMPLX_0, XXREAL_0, INT_1, RAT_1, COMPLEX1, FINSEQ_1, ABIAN, MATRIX_0, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_4, VECTSP_7, MATRIX_1, FVSUM_1, MATRIX_3, HAHNBAN1, INT_3, BILINEAR, ZMODUL01, ZMODUL03, GAUSSINT, ZMODUL04, ZMODUL06, ZMATRLIN;
definitions RLVECT_1, ALGSTR_0, VECTSP_1;
theorems BINOP_1, CARD_1, CARD_2, FINSEQ_1, FINSEQ_3, FUNCT_1, FUNCT_2, INT_1, NAT_1, RLVECT_1, TARSKI, ZMODUL01, ZFMISC_1, GAUSSINT, XTUPLE_0, ZMODUL03, HAHNBAN1, XBOOLE_0, XBOOLE_1, FUNCOP_1, XREAL_1, XXREAL_0, STRUCT_0, PARTFUN1, VECTSP_1, ALGSTR_0, EC_PF_1, ZMODUL02, VECTSP_7, NUMBERS, VECTSP_4, ABSVALUE, MATRIX_0, ZMODUL06, MATRIXR2, MATRIX_3, ZMATRLIN, FUNCT_5, VECTSP10, FVSUM_1, DOMAIN_1, MATRIX_4, MATRIX11, MATRIX_7, MATRIX_1;
schemes BINOP_1, FUNCT_2, NAT_1, MATRIX_0, FINSEQ_2;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0, STRUCT_0, RLVECT_1, VALUED_0, MEMBERED, FINSEQ_1, CARD_1, INT_1, ZMODUL01, XBOOLE_0, BINOP_2, ORDINAL1, XXREAL_0, NAT_1, ALGSTR_0, INT_3, REALSET1, RELAT_1, VECTSP_1, VECTSP_2, GAUSSINT, FUNCT_3, RAT_1, XCMPLX_0, ZMODUL03, ZMODUL04, ZMODUL05, ZMODUL06, ABIAN, MATRIX_0, ZMATRLIN;
constructors HIDDEN, BINOP_2, UPROOTS, ZMODUL01, REALSET1, EUCLID, FVSUM_1, FUNCT_3, ALGSTR_1, EC_PF_1, MATRIX_3, ZMODUL04, ZMODUL06, ABIAN, ZMATRLIN, ZMODUL07;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XCMPLX_0, BINOP_1, STRUCT_0, ALGSTR_0, INT_3, VECTSP_1, VECTSP_4, REALSET1, FVSUM_1, FUNCOP_1, FINSEQ_1, MATRIX_0, ZMATRLIN;
expansions TARSKI, STRUCT_0, VECTSP_1, BINOP_1, FINSEQ_1, HAHNBAN1, ZMATRLIN;
definition
let IT be non
empty LatticeStr over
INT.Ring ;
attr IT is
Z_Lattice-like means :
defZLattice:
( ( for
x being
Vector of
IT st ( for
y being
Vector of
IT holds
<;x,y;> = 0 ) holds
x = 0. IT ) & ( for
x,
y being
Vector of
IT holds
<;x,y;> = <;y,x;> ) & ( for
x,
y,
z being
Vector of
IT for
a being
Element of
INT.Ring holds
(
<;(x + y),z;> = <;x,z;> + <;y,z;> &
<;(a * x),y;> = a * <;x,y;> ) ) );
end;
::
deftheorem defZLattice defines
Z_Lattice-like ZMODLAT1:def 3 :
for IT being non empty LatticeStr over INT.Ring holds
( IT is Z_Lattice-like iff ( ( for x being Vector of IT st ( for y being Vector of IT holds <;x,y;> = 0 ) holds
x = 0. IT ) & ( for x, y being Vector of IT holds <;x,y;> = <;y,x;> ) & ( for x, y, z being Vector of IT
for a being Element of INT.Ring holds
( <;(x + y),z;> = <;x,z;> + <;y,z;> & <;(a * x),y;> = a * <;x,y;> ) ) ) );
ZMtoZL1:
for V being Z_Module
for sc being Function of [: the carrier of V, the carrier of V:], the carrier of F_Real holds
( GenLat (V,sc) is Abelian & GenLat (V,sc) is add-associative & GenLat (V,sc) is right_zeroed & GenLat (V,sc) is right_complementable & GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital )
registration
let V be
Z_Module;
let sc be
Function of
[: the carrier of V, the carrier of V:], the
carrier of
F_Real;
correctness
coherence
( GenLat (V,sc) is Abelian & GenLat (V,sc) is add-associative & GenLat (V,sc) is right_zeroed & GenLat (V,sc) is right_complementable & GenLat (V,sc) is scalar-distributive & GenLat (V,sc) is vector-distributive & GenLat (V,sc) is scalar-associative & GenLat (V,sc) is scalar-unital );
by ZMtoZL1;
end;
ZMtoZL2:
for V being free Z_Module
for sc being Function of [: the carrier of V, the carrier of V:], the carrier of F_Real holds GenLat (V,sc) is free
theorem ThNonTrivialLat1:
definition
let V,
W be non
empty ModuleStr over
INT.Ring ;
let f,
g be
FrForm of
V,
W;
existence
ex b1 being FrForm of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) + (g . (v,w))
uniqueness
for b1, b2 being FrForm of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) + (g . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = (f . (v,w)) + (g . (v,w)) ) holds
b1 = b2
end;
definition
let V,
W be non
empty ModuleStr over
INT.Ring ;
let f be
FrForm of
V,
W;
let a be
Element of
F_Real;
existence
ex b1 being FrForm of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = a * (f . (v,w))
uniqueness
for b1, b2 being FrForm of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = a * (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = a * (f . (v,w)) ) holds
b1 = b2
end;
definition
let V,
W be non
empty ModuleStr over
INT.Ring ;
let f be
FrForm of
V,
W;
existence
ex b1 being FrForm of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = - (f . (v,w))
uniqueness
for b1, b2 being FrForm of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = - (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = - (f . (v,w)) ) holds
b1 = b2
end;
definition
let V,
W be non
empty ModuleStr over
INT.Ring ;
let f,
g be
FrForm of
V,
W;
redefine func f - g means :
Def7:
for
v being
Vector of
V for
w being
Vector of
W holds
it . (
v,
w)
= (f . (v,w)) - (g . (v,w));
compatibility
for b1 being FrForm of V,W holds
( b1 = f - g iff for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) - (g . (v,w)) )
end;
theorem
for
V,
W being non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ModuleStr over
INT.Ring for
v,
u being
Vector of
V for
w,
t being
Vector of
W for
a,
b being
Element of
INT.Ring for
f being
bilinear-FrForm of
V,
W holds
f . (
(v + (a * u)),
(w + (b * t)))
= ((f . (v,w)) + (b * (f . (v,t)))) + ((a * (f . (u,w))) + (a * (b * (f . (u,t)))))
theorem
for
V,
W being
Z_Module for
v,
u being
Vector of
V for
w,
t being
Vector of
W for
a,
b being
Element of
INT.Ring for
f being
bilinear-FrForm of
V,
W holds
f . (
(v - (a * u)),
(w - (b * t)))
= ((f . (v,w)) - (b * (f . (v,t)))) - ((a * (f . (u,w))) - (a * (b * (f . (u,t)))))
definition
let V1,
V2 be
free finite-rank Z_Module;
let b1 be
OrdBasis of
V1;
let b2 be
OrdBasis of
V2;
let f be
bilinear-FrForm of
V1,
V2;
existence
ex b1 being Matrix of len b1, len b2,F_Real st
for i, j being Nat st i in dom b1 & j in dom b2 holds
b1 * (i,j) = f . ((b1 /. i),(b2 /. j))
uniqueness
for b1, b2 being Matrix of len b1, len b2,F_Real st ( for i, j being Nat st i in dom b1 & j in dom b2 holds
b1 * (i,j) = f . ((b1 /. i),(b2 /. j)) ) & ( for i, j being Nat st i in dom b1 & j in dom b2 holds
b2 * (i,j) = f . ((b1 /. i),(b2 /. j)) ) holds
b1 = b2
end;
theorem MLT1:
for
m,
l,
n being
Nat for
S being
Matrix of
l,
m,
INT.Ring for
T being
Matrix of
m,
n,
INT.Ring for
S1 being
Matrix of
l,
m,
F_Real for
T1 being
Matrix of
m,
n,
F_Real st
S = S1 &
T = T1 &
0 < l &
0 < m holds
S * T = S1 * T1
theorem ThMBF3:
for
V being
free finite-rank Z_Module for
b1,
b2 being
OrdBasis of
V for
f being
bilinear-FrForm of
V,
V st
0 < rank V holds
BilinearM (
f,
b2,
b2)
= ((inttorealM (AutMt ((id V),b2,b1))) * (BilinearM (f,b1,b1))) * ((inttorealM (AutMt ((id V),b2,b1))) @)
ThIntLatZ:
for L being INTegral Z_Lattice holds GramDet L is Integer