:: Embedded Lattice and Properties of {G}ram Matrix
:: by Yuichi Futa and Yasunari Shidama
::
:: Received March 17, 2017
:: Copyright (c) 2017-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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, ARYTM_1, NAT_1,
FINSET_1, FUNCOP_1, RLSUB_1, QC_LANG1, BINOP_1, ZFMISC_1, INT_1,
RLVECT_2, ZMODUL01, ZMODUL03, RLVECT_3, RMOD_2, RANKNULL, FINSEQ_2,
UPROOTS, GROUP_1, INT_3, VECTSP_1, MESFUNC1, XCMPLX_0, FUNCSDOM,
REALSET1, MATRLIN, ZMODUL02, RLVECT_5, NORMSP_1, BHSP_1, MATRIX_1,
MATRIX_3, MOD_3, ZMATRLIN, ZMODLAT1, TREES_1, MFOLD_2, ZMODUL04,
ZMODUL08, FUNCT_2, ZMODLAT2, VECTSP10, VECTSP_2, MSAFREE2, EQREL_1,
VALUED_1, INT_2, RELAT_2, LAPLACE, CLASSES1, LMOD_7, PRVECT_1, MATRIX13;
notations 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, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, RAT_1, INT_2,
FINSEQ_1, FINSEQ_2, EQREL_1, MATRIX_0, STRUCT_0, ALGSTR_0, RLVECT_1,
GROUP_1, VECTSP_1, PRVECT_1, VECTSP_2, VECTSP_4, VECTSP_6, VECTSP_7,
RANKNULL, MATRIX_1, MATRIX_3, INT_3, ZMODUL01, ZMODUL03, GAUSSINT,
ZMODUL04, ZMATRLIN, ZMODLAT1, ZMODUL08, MATRIX_6, LAPLACE, NAT_D,
MATRIX13;
constructors BINOP_2, UPROOTS, REALSET1, ALGSTR_1, ZMODUL01, EC_PF_1,
ZMODUL04, ZMODUL07, ZMODLAT1, ZMODUL08, MATRIX_6, LAPLACE, MATRIX13,
RELSET_1, FVSUM_1;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, 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, INT_3, REALSET1,
RELAT_1, VECTSP_1, GAUSSINT, RAT_1, XCMPLX_0, ZMODUL03, ZMODUL04,
ZMODUL05, ZMODUL06, MATRIX_0, ZMODLAT1, ZMODUL08, PRVECT_1, MATRIX13;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
theorem :: ZMODLAT2:1
for K being Ring,
V being LeftMod of K,
L being Function of the carrier of V, the carrier of K,
A being Subset of V,
F, F1 being FinSequence of the carrier of V
st F is one-to-one & rng F = A
& F1 is one-to-one & rng F1 = A
holds Sum(L (#) F) = Sum(L (#) F1);
theorem :: ZMODLAT2:2
for K being Ring, V being LeftMod of K, A being finite Subset of V
holds
A is linearly-independent
iff
( for L being Linear_Combination of A
st ( ex F being FinSequence of the carrier of V
st F is one-to-one & rng F = A
& Sum(L (#) F) = 0.V)
holds Carrier(L) = {});
theorem :: ZMODLAT2:3
for K being Ring,
V being LeftMod of K,
b being FinSequence of V
st b is one-to-one
holds
( rng b is linearly-independent
iff
for r being FinSequence of K,
rb being FinSequence of V
st len r = len b & len rb = len b
& ( for i be Nat st i in dom rb holds rb.i = r/.i * b/.i)
& Sum (rb) = 0.V
holds r = Seg (len r) --> 0.K);
theorem :: ZMODLAT2:4
for K being Ring, V being LeftMod of K, A being finite Subset of V
holds
A is linearly-independent
iff
ex b being FinSequence of V
st b is one-to-one & rng b = A &
for r being FinSequence of K,
rb being FinSequence of V
st len r = len b & len rb = len b &
( for i being Nat st i in dom rb holds rb.i = r/.i * b/.i) &
Sum (rb) = 0.V
holds r = Seg (len r) --> 0.K;
registration
let V be non trivial free Z_Module;
cluster -> non empty for Basis of V;
end;
definition
let IT be Z_Lattice;
attr IT is RATional means
:: ZMODLAT2:def 1
for v, u being Vector of IT holds <; v, u ;> in RAT;
end;
registration
cluster non trivial RATional positive-definite for Z_Lattice;
end;
registration
let L be RATional Z_Lattice;
let v, u be Vector of L;
cluster <; v, u ;> -> rational;
end;
registration
cluster -> RATional for INTegral Z_Lattice;
end;
definition
let L be Z_Lattice;
func ScProductEM(L) -> Function of
[:the carrier of EMbedding(L), the carrier of EMbedding(L):],
the carrier of F_Real means
:: ZMODLAT2:def 2
for v, u being Vector of L, vv, uu being Vector of EMbedding(L)
st vv = (MorphsZQ(L)).v & uu = (MorphsZQ(L)).u holds
it.(vv, uu) = <; v, u ;>;
end;
theorem :: ZMODLAT2:5
for L being Z_Lattice holds
(for x being Vector of EMbedding(L)
st for y being Vector of EMbedding(L) holds (ScProductEM(L)).(x, y) = 0
holds x = 0.(EMbedding(L))) &
(for x, y being Vector of EMbedding(L)
holds (ScProductEM(L)).(x, y) = (ScProductEM(L)).(y, x)) &
(for x, y, z being Vector of EMbedding(L), a being Element of INT.Ring
holds (ScProductEM(L)).(x+y, z) =
(ScProductEM(L)).(x, z) + (ScProductEM(L)).(y, z)
& (ScProductEM(L)).(a*x, y) = a * (ScProductEM(L)).(x, y));
definition
let L be Z_Lattice;
func ScProductDM(L) -> Function of
[:the carrier of DivisibleMod(L), the carrier of DivisibleMod(L):],
the carrier of F_Real means
:: ZMODLAT2:def 3
for vv, uu being Vector of DivisibleMod(L),
v, u being Vector of EMbedding(L), a, b being Element of INT.Ring,
ai, bi being Element of F_Real
st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu
holds it.(vv, uu) = ai" * bi" * (ScProductEM(L)).(v, u);
end;
theorem :: ZMODLAT2:6
for L being Z_Lattice holds
(for x being Vector of DivisibleMod(L)
st for y being Vector of DivisibleMod(L) holds (ScProductDM(L)).(x, y) = 0
holds x = 0.(DivisibleMod(L))) &
(for x, y being Vector of DivisibleMod(L)
holds (ScProductDM(L)).(x, y) = (ScProductDM(L)).(y, x)) &
(for x, y, z being Vector of DivisibleMod(L), a being Element of INT.Ring
holds (ScProductDM(L)).(x+y, z) =
(ScProductDM(L)).(x, z) + (ScProductDM(L)).(y, z)
& (ScProductDM(L)).(a*x, y) = a * (ScProductDM(L)).(x, y));
theorem :: ZMODLAT2:7
for L being Z_Lattice holds
ScProductEM(L) = (ScProductDM(L)) || (rng MorphsZQ(L));
theorem :: ZMODLAT2:8
for L being Z_Lattice, v1, v2 being Vector of DivisibleMod(L),
u1, u2 being Vector of EMbedding(L) st v1 = u1 & v2 = u2 holds
(ScProductEM(L)).(u1, u2) = (ScProductDM(L)).(v1, v2);
theorem :: ZMODLAT2:9
for L being Z_Lattice, r being Element of F_Rat,
v, u being Vector of EMbedding(r, L) holds
((ScProductDM(L)) || (the carrier of EMbedding(r, L))).(v, u)
= (ScProductDM(L)).(v, u);
theorem :: ZMODLAT2:10
for L being Z_Lattice, A being non empty set, ze being Element of A,
ad being BinOp of A,
mu being Function of [:the carrier of INT.Ring, A:],A,
sc being Function of [:A, A:],the carrier of F_Real
st A is linearly-closed Subset of DivisibleMod(L) & ze = 0.DivisibleMod(L) &
ad = (the addF of DivisibleMod(L)) || A &
mu = (the lmult of DivisibleMod(L)) | [:the carrier of INT.Ring, A:] holds
LatticeStr (# A, ad, ze,mu, sc #) is Submodule of DivisibleMod(L);
theorem :: ZMODLAT2:11
for L being Z_Lattice, v, u being Vector of DivisibleMod(L) holds
(ScProductDM(L)).(-v, u) = -(ScProductDM(L)).(v, u) &
(ScProductDM(L)).(u, -v) = -(ScProductDM(L)).(u, v);
theorem :: ZMODLAT2:12
for L being Z_Lattice, v, u, w being Vector of DivisibleMod(L) holds
(ScProductDM(L)).(v, u + w)
= (ScProductDM(L)).(v, u) + (ScProductDM(L)).(v, w);
theorem :: ZMODLAT2:13
for L being Z_Lattice, v, u being Vector of DivisibleMod(L),
a being Element of INT.Ring
holds (ScProductDM(L)).(v, a*u) = a * (ScProductDM(L)).(v, u);
theorem :: ZMODLAT2:14
for L being Z_Lattice, v being Vector of DivisibleMod(L) holds
(ScProductDM(L)).(0.DivisibleMod(L), v) = 0 &
(ScProductDM(L)).(v, 0.DivisibleMod(L)) = 0;
theorem :: ZMODLAT2:15
for L being Z_Lattice,
v being Vector of DivisibleMod(L), I being Basis of EMbedding(L)
st for u being Vector of DivisibleMod(L) st u in I
holds (ScProductDM(L)).(v, u) = 0 holds
for u being Vector of DivisibleMod(L) holds (ScProductDM(L)).(v, u) = 0;
theorem :: ZMODLAT2:16
for L being Z_Lattice,
v being Vector of DivisibleMod(L), I being Basis of EMbedding(L)
st for u being Vector of DivisibleMod(L) st u in I
holds (ScProductDM(L)).(v, u) = 0
holds v = 0.DivisibleMod(L);
theorem :: ZMODLAT2:17
for R being Ring, V being LeftMod of R, v being Vector of V,
u being object st u in Lin{v} holds
ex i being Element of R st u = i*v;
theorem :: ZMODLAT2:18
for R being Ring, V being LeftMod of R, v being Vector of V holds
v in Lin{v};
theorem :: ZMODLAT2:19
for R being Ring, V being LeftMod of R, v being Vector of V,
i being Element of R holds i*v in Lin{v};
begin :: 2. Embedding of lattice
definition
let L be Z_Lattice;
func EMLat(L) -> strict Z_Lattice means
:: ZMODLAT2:def 4
the carrier of it = rng MorphsZQ(L) &
the ZeroF of it = zeroCoset(L) &
the addF of it = (addCoset(L)) || (rng MorphsZQ(L)) &
the lmult of it = (lmultCoset(L)) | [:the carrier of INT.Ring,
rng MorphsZQ(L):] &
the scalar of it = ScProductEM(L);
end;
definition
let L be Z_Lattice;
let r be Element of F_Rat;
func EMLat(r, L) -> strict Z_Lattice means
:: ZMODLAT2:def 5
the carrier of it = r * (rng MorphsZQ(L)) &
the ZeroF of it = zeroCoset(L) &
the addF of it = (addCoset(L)) || ( r * (rng MorphsZQ(L))) &
the lmult of it = (lmultCoset(L)) |
[:the carrier of INT.Ring, r * (rng MorphsZQ(L)):] &
the scalar of it = (ScProductDM(L)) || (r * (rng MorphsZQ(L)));
end;
registration
let L be non trivial Z_Lattice;
cluster EMLat(L) -> non trivial;
end;
registration
let L be non trivial Z_Lattice, r be non zero Element of F_Rat;
cluster EMLat(r,L) -> non trivial;
end;
registration
let L be INTegral Z_Lattice;
cluster EMLat(L) -> INTegral;
end;
theorem :: ZMODLAT2:20
for L being Z_Lattice holds EMLat(L) is Submodule of DivisibleMod(L);
theorem :: ZMODLAT2:21
for L being Z_Lattice, r being Element of F_Rat holds
EMLat(r, L) is Submodule of DivisibleMod(L);
theorem :: ZMODLAT2:22
for L being Z_Lattice, r being non zero Element of F_Rat,
m, n being Element of INT.Ring, m1,n1 being Element of INT,
v being Vector of EMLat(r, L)
st m = m1 & n = n1 & r = m1/n1 & n1 <> 0
holds ex x being Vector of EMLat(L) st n*v = m*x;
theorem :: ZMODLAT2:23
for L being Z_Lattice, r being Element of F_Rat,
v, u being Vector of EMLat(r, L), x, y being Vector of EMLat(L)
st v = x & u = y holds <; v, u ;> = <; x, y ;>;
theorem :: ZMODLAT2:24
for L being INTegral Z_Lattice, r being non zero Element of F_Rat,
a being Rational, v, u being Vector of EMLat(r, L)
st r = a holds
a" * a" * <; v, u ;> in INT;
registration
let L be positive-definite Z_Lattice;
cluster EMLat(L) -> positive-definite;
end;
registration
let L be positive-definite Z_Lattice;
let r be non zero Element of F_Rat;
cluster EMLat(r, L) -> positive-definite;
end;
theorem :: ZMODLAT2:25
for L being positive-definite Z_Lattice,
v being Vector of DivisibleMod(L) holds
(ScProductDM(L)).(v, v) = 0 iff v = 0.DivisibleMod(L);
theorem :: ZMODLAT2:26
for L being positive-definite Z_Lattice,
Z being non empty LatticeStr over INT.Ring st
Z is Submodule of DivisibleMod(L) &
the scalar of Z = (ScProductDM(L)) || (the carrier of Z) holds
Z is Z_Lattice-like;
theorem :: ZMODLAT2:27
for L being positive-definite Z_Lattice,
Z being non empty LatticeStr over INT.Ring
st Z is finitely-generated Submodule of DivisibleMod(L) &
the scalar of Z = (ScProductDM(L)) || (the carrier of Z) holds
Z is Z_Lattice;
theorem :: ZMODLAT2:28
for L being Z_Lattice holds
the ModuleStr of EMLat(L) = EMbedding(L);
theorem :: ZMODLAT2:29
for L, E being Z_Module st the ModuleStr of L = the ModuleStr of E
holds L is Submodule of E;
theorem :: ZMODLAT2:30
for E, L being Z_Module, I being Subset of L, J being Subset of E,
K being Linear_Combination of J
st I = J & the ModuleStr of L = the ModuleStr of E
holds K is Linear_Combination of I;
theorem :: ZMODLAT2:31
for E, L being Z_Module,
K being Linear_Combination of E,
H being Linear_Combination of L
st K = H & the ModuleStr of L = the ModuleStr of E
holds Carrier K = Carrier H;
theorem :: ZMODLAT2:32
for E, L being Z_Module,
K being Linear_Combination of E,
H being Linear_Combination of L
st K = H & the ModuleStr of L = the ModuleStr of E
holds Sum K = Sum H;
theorem :: ZMODLAT2:33
for L, E being Z_Module, I being Subset of L, J being Subset of E
st the ModuleStr of L = the ModuleStr of E & I = J
holds (I is linearly-independent iff J is linearly-independent);
theorem :: ZMODLAT2:34
for L, E being Z_Module, I being Subset of L, J be Subset of E
st the ModuleStr of L = the ModuleStr of E & I = J
holds Lin I = Lin J;
theorem :: ZMODLAT2:35
for L, E being free Z_Module, I being Subset of L, J being Subset of E
st the ModuleStr of L = the ModuleStr of E & I = J
holds ( I is Basis of L iff J is Basis of E);
theorem :: ZMODLAT2:36
for L, E being finite-rank free Z_Module
st the ModuleStr of L = the ModuleStr of E
holds rank L = rank E;
theorem :: ZMODLAT2:37
for L being Z_Lattice, I being Subset of L
holds I is Basis of L
iff (MorphsZQ(L)).: I is Basis of EMbedding(L);
theorem :: ZMODLAT2:38
for L being Z_Lattice, I being Subset of L
holds I is Basis of L
iff (MorphsZQ(L)).: I is Basis of EMLat(L);
theorem :: ZMODLAT2:39
for L being Z_Lattice, b being FinSequence of L
holds b is OrdBasis of L
iff (MorphsZQ(L))*b is OrdBasis of EMbedding(L);
theorem :: ZMODLAT2:40
for L being Z_Lattice,
E being finite-rank free Z_Module,
I being FinSequence of L,
J being FinSequence of E
st the ModuleStr of L = the ModuleStr of E & I = J
holds ( I is OrdBasis of L iff J is OrdBasis of E);
theorem :: ZMODLAT2:41
for L being Z_Lattice, b being FinSequence of L
holds b is OrdBasis of L
iff (MorphsZQ(L))*b is OrdBasis of EMLat(L);
theorem :: ZMODLAT2:42
for L being Z_Lattice holds rank (L) = rank(EMLat(L));
theorem :: ZMODLAT2:43
for L being Z_Lattice, x being object holds
x is Vector of EMLat(L) iff x is Vector of EMbedding(L);
registration
let L be RATional Z_Lattice;
let v, u be Vector of EMLat(L);
cluster (ScProductEM(L)).(v, u) -> rational;
end;
registration
let L be RATional Z_Lattice;
let v, u be Vector of DivisibleMod(L);
cluster (ScProductDM(L)).(v, u) -> rational;
end;
begin :: 3. Properties of Gram Matrix
definition
let V be ModuleStr over INT.Ring;
let f be FrForm of V,V;
attr f is symmetric means
:: ZMODLAT2:def 6
for v, w being Vector of V holds f.(v, w) = f.(w, v);
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster NulFrForm(V,V) -> symmetric;
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster symmetric for FrForm of V, V;
end;
registration
let V be non empty ModuleStr over INT.Ring;
cluster symmetric for bilinear-FrForm of V, V;
end;
registration
let L be Z_Lattice;
cluster InnerProduct(L) -> symmetric;
end;
registration
let V be finite-rank free Z_Module;
let f be symmetric bilinear-FrForm of V, V;
let b be OrdBasis of V;
cluster GramMatrix(f, b) -> symmetric;
end;
theorem :: ZMODLAT2:44
for L being RATional Z_Lattice,
v, u being Vector of DivisibleMod(L)
holds (ScProductDM(L)).(v, u) in F_Rat;
theorem :: ZMODLAT2:45
for L being RATional Z_Lattice, b being OrdBasis of L holds
GramMatrix(b) is Matrix of dim(L),F_Rat;
theorem :: ZMODLAT2:46
for F being FinSequence of F_Real, G being FinSequence of F_Rat st F = G
holds Sum F = Sum G;
theorem :: ZMODLAT2:47
for i being Nat, j being Element of F_Real, k being Element of F_Rat
st j = k
holds power(F_Real).(-1_F_Real,i)*j = power(F_Rat).(-1_F_Rat,i)*k;
theorem :: ZMODLAT2:48
for F being FinSequence of F_Real
st for i being Nat st i in dom F holds F.i in F_Rat
holds Sum F in F_Rat;
theorem :: ZMODLAT2:49
for i being Nat holds power(F_Real).(-1_F_Real,i) in F_Rat;
theorem :: ZMODLAT2:50
for n, i, j, k, m being Nat, M being Matrix of n+1,F_Real
for L being Matrix of n+1,F_Rat
st 0 < n & M = L &
[i, j] in Indices M & [k, m] in Indices (Delete(M,i,j))
holds (Delete(M,i,j))*(k,m) = (Delete(L,i,j))*(k,m);
theorem :: ZMODLAT2:51
for n, i, j, k, m being Nat, M being Matrix of n+1, F_Real
st 0 < n & M is Matrix of n+1, F_Rat &
[i, j] in Indices M & [k, m] in Indices (Delete(M,i,j))
holds (Delete(M,i,j))*(k,m) is Element of F_Rat;
theorem :: ZMODLAT2:52
for n, i, j being Nat, M being Matrix of n+1, F_Real
for L being Matrix of n+1, F_Rat
st 0 < n & M = L & [i, j] in Indices M
holds Delete(M,i,j) = Delete(L,i,j);
theorem :: ZMODLAT2:53
for n, i, j being Nat, M being Matrix of n+1, F_Real
st 0 < n & M is Matrix of n+1,F_Rat & [i, j] in Indices M
holds Delete(M,i,j) is Matrix of n, F_Rat;
theorem :: ZMODLAT2:54
for n being Nat, M being Matrix of n, F_Real
for H being Matrix of n, F_Rat
st M = H
holds Det M = Det H;
theorem :: ZMODLAT2:55
for n being Nat, M being Matrix of n, F_Real st M is Matrix of n, F_Rat
holds Det M in F_Rat;
theorem :: ZMODLAT2:56
for n, i, j being Nat, M being Matrix of n+1, F_Real
st M is Matrix of n+1, F_Rat & [i, j] in Indices M
holds Cofactor(M,i,j) in F_Rat;
theorem :: ZMODLAT2:57
for L being RATional Z_Lattice, b being OrdBasis of L holds
Det GramMatrix(b) in F_Rat;
theorem :: ZMODLAT2:58
for L being positive-definite Z_Lattice, I being Basis of L,
v, w being Vector of L holds
(for u being Vector of L st u in I holds <; u, v ;> = <; u, w ;>)
implies
(for u being Vector of L holds <; u, v ;> = <; u, w ;>);
theorem :: ZMODLAT2:59
for L being positive-definite Z_Lattice, b being OrdBasis of L,
v, w being Vector of L
st for n being Nat st n in dom b holds <; b/.n, v ;> = <; b/.n, w ;>
holds v = w;
theorem :: ZMODLAT2:60
for n being Nat, M being Matrix of n, F_Rat
st M is without_repeated_line
holds Det M <> 0.F_Rat iff lines M is linearly-independent;
theorem :: ZMODLAT2:61
for L being positive-definite Z_Lattice, I being Basis of L,
v, w being Vector of L holds
(for u being Vector of L st u in I holds <; v,u ;> = <; w,u ;>)
implies
(for u being Vector of L holds <; v,u ;> = <; w,u;>);
theorem :: ZMODLAT2:62
for L being positive-definite Z_Lattice, b being OrdBasis of L,
v, w being Vector of L
st for n being Nat st n in dom b holds <; v, b/.n;> = <; w, b/.n ;>
holds v = w;
theorem :: ZMODLAT2:63
for L being positive-definite Z_Lattice, b being OrdBasis of EMLat(L),
v, w being Vector of DivisibleMod(L)
st for n being Nat st n in dom b holds
(ScProductDM(L)).(b/.n, v) = (ScProductDM(L)).(b/.n, w)
holds v = w;
theorem :: ZMODLAT2:64
for L being positive-definite Z_Lattice, b being OrdBasis of EMLat(L),
v, w being Vector of DivisibleMod(L)
st for n being Nat st n in dom b holds
(ScProductDM(L)).(v, b/.n) = (ScProductDM(L)).(w, b/.n)
holds v = w;
theorem :: ZMODLAT2:65
for L being non trivial RATional
positive-definite Z_Lattice,
v being Element of L,
b being FinSequence of L,
sbv being FinSequence of F_Rat
st len b = len sbv
& for n being Nat st n in dom sbv
holds sbv.n = <; b/.n, v ;>
holds <; Sum (b), v ;> = Sum sbv;
theorem :: ZMODLAT2:66
for n being Nat, r being FinSequence of F_Rat st len r = n
holds
ex K being Integer, Kr being FinSequence of INT.Ring
st K <> 0 & len Kr = n
& for i being Nat st i in dom Kr
holds Kr.i = K * r/.i;
theorem :: ZMODLAT2:67
for i, j being Nat
for K being Field
for a, aj being Element of K
for R being Element of i-VectSp_over K
st j in Seg i & aj = R.j holds
(a * R).j = a * aj;
theorem :: ZMODLAT2:68
for i, j being Nat
for K being Field
for aj, bj being Element of K
for A,B being Element of i-VectSp_over K
st j in Seg i & aj = A.j & bj = B.j holds
(A+B).j = aj + bj;
theorem :: ZMODLAT2:69
for K being Field, n, i being Nat st i in Seg n holds
for s being FinSequence of n-VectSp_over K holds
ex si being FinSequence of K
st len si = len s & Sum(s).i = Sum(si)
& for k being Nat st k in dom si holds si.k = (s/.k).i;
theorem :: ZMODLAT2:70
for L being non trivial RATional positive-definite Z_Lattice,
b being OrdBasis of L holds
Det GramMatrix(b) <> 0.F_Real;
registration
let L be non trivial RATional positive-definite Z_Lattice;
let b be OrdBasis of L;
cluster GramMatrix(b) -> invertible;
end;