:: Embedded Lattice and Properties of {G}ram Matrix :: by Yuichi Futa and Yasunari Shidama :: :: Received March 17, 2017 :: Copyright (c) 2017-2021 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;