:: Dual Lattice of $\mathbb Z$-module Lattice
:: by Yuichi Futa and Yasunari Shidama
::
:: Copyright (c) 2017-2019 Association of Mizar Users

theorem ThSLGM1: :: ZMODLAT3:1
for L being RATional Z_Lattice
for LX being Z_Lattice st LX is Submodule of DivisibleMod L & the scalar of LX = () || the carrier of LX holds
LX is RATional
proof end;

registration
let L be RATional Z_Lattice;
correctness
coherence ;
proof end;
end;

registration
let L be RATional Z_Lattice;
let r be Element of F_Rat;
cluster EMLat (r,L) -> RATional ;
correctness
coherence
EMLat (r,L) is RATional
;
proof end;
end;

definition
let L be Z_Lattice;
let F be FinSequence of L;
let f be Function of L,INT.Ring;
let v be Vector of L;
func ScFS (v,f,F) -> FinSequence of F_Real means :defScFS: :: ZMODLAT3:def 1
( len it = len F & ( for i being Nat st i in dom it holds
it . i = <;v,((f . (F /. i)) * (F /. i));> ) );
existence
ex b1 being FinSequence of F_Real st
( len b1 = len F & ( for i being Nat st i in dom b1 holds
b1 . i = <;v,((f . (F /. i)) * (F /. i));> ) )
proof end;
uniqueness
for b1, b2 being FinSequence of F_Real st len b1 = len F & ( for i being Nat st i in dom b1 holds
b1 . i = <;v,((f . (F /. i)) * (F /. i));> ) & len b2 = len F & ( for i being Nat st i in dom b2 holds
b2 . i = <;v,((f . (F /. i)) * (F /. i));> ) holds
b1 = b2
proof end;
end;

:: deftheorem defScFS defines ScFS ZMODLAT3:def 1 :
for L being Z_Lattice
for F being FinSequence of L
for f being Function of L,INT.Ring
for v being Vector of L
for b5 being FinSequence of F_Real holds
( b5 = ScFS (v,f,F) iff ( len b5 = len F & ( for i being Nat st i in dom b5 holds
b5 . i = <;v,((f . (F /. i)) * (F /. i));> ) ) );

theorem ThScFS1: :: ZMODLAT3:2
for L being Z_Lattice
for f being Function of L,INT.Ring
for F being FinSequence of L
for v, u being Vector of L
for i being Nat st i in dom F & u = F . i holds
(ScFS (v,f,F)) . i = <;v,((f . u) * u);>
proof end;

theorem ThScFS3: :: ZMODLAT3:3
for L being Z_Lattice
for f being Function of L,INT.Ring
for v, u being Vector of L holds ScFS (v,f,<*u*>) = <*<;v,((f . u) * u);>*>
proof end;

theorem ThScFS6: :: ZMODLAT3:4
for L being Z_Lattice
for f being Function of L,INT.Ring
for F, G being FinSequence of L
for v being Vector of L holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))
proof end;

definition
let L be Z_Lattice;
let l be Linear_Combination of L;
let v be Vector of L;
func SumSc (v,l) -> Element of F_Real means :defSumSc: :: ZMODLAT3:def 2
ex F being FinSequence of L st
( F is one-to-one & rng F = Carrier l & it = Sum (ScFS (v,l,F)) );
existence
ex b1 being Element of F_Real ex F being FinSequence of L st
( F is one-to-one & rng F = Carrier l & b1 = Sum (ScFS (v,l,F)) )
proof end;
uniqueness
for b1, b2 being Element of F_Real st ex F being FinSequence of L st
( F is one-to-one & rng F = Carrier l & b1 = Sum (ScFS (v,l,F)) ) & ex F being FinSequence of L st
( F is one-to-one & rng F = Carrier l & b2 = Sum (ScFS (v,l,F)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defSumSc defines SumSc ZMODLAT3:def 2 :
for L being Z_Lattice
for l being Linear_Combination of L
for v being Vector of L
for b4 being Element of F_Real holds
( b4 = SumSc (v,l) iff ex F being FinSequence of L st
( F is one-to-one & rng F = Carrier l & b4 = Sum (ScFS (v,l,F)) ) );

theorem LmSumSc11: :: ZMODLAT3:5
for L being Z_Lattice
for v being Vector of L holds SumSc (v,()) = 0. F_Real
proof end;

theorem :: ZMODLAT3:6
for L being Z_Lattice
for v being Vector of L
for l being Linear_Combination of {} the carrier of L holds SumSc (v,l) = 0. F_Real
proof end;

theorem LmSumSc13: :: ZMODLAT3:7
for L being Z_Lattice
for v being Vector of L
for l being Linear_Combination of L st Carrier l = {} holds
SumSc (v,l) = 0. F_Real
proof end;

theorem LmSumSc14: :: ZMODLAT3:8
for L being Z_Lattice
for v, u being Vector of L
for l being Linear_Combination of {u} holds SumSc (v,l) = <;v,((l . u) * u);>
proof end;

theorem LmSumSc1X: :: ZMODLAT3:9
for L being Z_Lattice
for v being Vector of L
for l1, l2 being Linear_Combination of L holds SumSc (v,(l1 + l2)) = (SumSc (v,l1)) + (SumSc (v,l2))
proof end;

theorem ThSumSc1: :: ZMODLAT3:10
for L being Z_Lattice
for l being Linear_Combination of L
for v being Vector of L holds <;v,(Sum l);> = SumSc (v,l)
proof end;

definition
let L be Z_Lattice;
let F be FinSequence of ();
let f be Function of (),INT.Ring;
let v be Vector of ();
func ScFS (v,f,F) -> FinSequence of F_Real means :defScFSDM: :: ZMODLAT3:def 3
( len it = len F & ( for i being Nat st i in dom it holds
it . i = () . (v,((f . (F /. i)) * (F /. i))) ) );
existence
ex b1 being FinSequence of F_Real st
( len b1 = len F & ( for i being Nat st i in dom b1 holds
b1 . i = () . (v,((f . (F /. i)) * (F /. i))) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of F_Real st len b1 = len F & ( for i being Nat st i in dom b1 holds
b1 . i = () . (v,((f . (F /. i)) * (F /. i))) ) & len b2 = len F & ( for i being Nat st i in dom b2 holds
b2 . i = () . (v,((f . (F /. i)) * (F /. i))) ) holds
b1 = b2
proof end;
end;

:: deftheorem defScFSDM defines ScFS ZMODLAT3:def 3 :
for L being Z_Lattice
for F being FinSequence of ()
for f being Function of (),INT.Ring
for v being Vector of ()
for b5 being FinSequence of F_Real holds
( b5 = ScFS (v,f,F) iff ( len b5 = len F & ( for i being Nat st i in dom b5 holds
b5 . i = () . (v,((f . (F /. i)) * (F /. i))) ) ) );

theorem ThScFSDM1: :: ZMODLAT3:11
for L being Z_Lattice
for f being Function of (),INT.Ring
for F being FinSequence of ()
for v, u being Vector of ()
for i being Nat st i in dom F & u = F . i holds
(ScFS (v,f,F)) . i = () . (v,((f . u) * u))
proof end;

theorem ThScFSDM3: :: ZMODLAT3:12
for L being Z_Lattice
for f being Function of (),INT.Ring
for v, u being Vector of () holds ScFS (v,f,<*u*>) = <*(() . (v,((f . u) * u)))*>
proof end;

theorem ThScFSDM6: :: ZMODLAT3:13
for L being Z_Lattice
for f being Function of (),INT.Ring
for F, G being FinSequence of ()
for v being Vector of () holds ScFS (v,f,(F ^ G)) = (ScFS (v,f,F)) ^ (ScFS (v,f,G))
proof end;

definition
let L be Z_Lattice;
let l be Linear_Combination of DivisibleMod L;
let v be Vector of ();
func SumSc (v,l) -> Element of F_Real means :defSumScDM: :: ZMODLAT3:def 4
ex F being FinSequence of () st
( F is one-to-one & rng F = Carrier l & it = Sum (ScFS (v,l,F)) );
existence
ex b1 being Element of F_Real ex F being FinSequence of () st
( F is one-to-one & rng F = Carrier l & b1 = Sum (ScFS (v,l,F)) )
proof end;
uniqueness
for b1, b2 being Element of F_Real st ex F being FinSequence of () st
( F is one-to-one & rng F = Carrier l & b1 = Sum (ScFS (v,l,F)) ) & ex F being FinSequence of () st
( F is one-to-one & rng F = Carrier l & b2 = Sum (ScFS (v,l,F)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defSumScDM defines SumSc ZMODLAT3:def 4 :
for L being Z_Lattice
for l being Linear_Combination of DivisibleMod L
for v being Vector of ()
for b4 being Element of F_Real holds
( b4 = SumSc (v,l) iff ex F being FinSequence of () st
( F is one-to-one & rng F = Carrier l & b4 = Sum (ScFS (v,l,F)) ) );

theorem LmSumScDM11: :: ZMODLAT3:14
for L being Z_Lattice
for v being Vector of () holds SumSc (v,()) = 0. F_Real
proof end;

theorem :: ZMODLAT3:15
for L being Z_Lattice
for v being Vector of ()
for l being Linear_Combination of {} the carrier of () holds SumSc (v,l) = 0. F_Real
proof end;

theorem LmSumScDM13: :: ZMODLAT3:16
for L being Z_Lattice
for v being Vector of ()
for l being Linear_Combination of DivisibleMod L st Carrier l = {} holds
SumSc (v,l) = 0. F_Real
proof end;

theorem LmSumScDM14: :: ZMODLAT3:17
for L being Z_Lattice
for v, u being Vector of ()
for l being Linear_Combination of {u} holds SumSc (v,l) = () . (v,((l . u) * u))
proof end;

theorem LmSumScDM1X: :: ZMODLAT3:18
for L being Z_Lattice
for v being Vector of ()
for l1, l2 being Linear_Combination of DivisibleMod L holds SumSc (v,(l1 + l2)) = (SumSc (v,l1)) + (SumSc (v,l2))
proof end;

theorem ThSumScDM1: :: ZMODLAT3:19
for L being Z_Lattice
for l being Linear_Combination of DivisibleMod L
for v being Vector of () holds () . (v,(Sum l)) = SumSc (v,l)
proof end;

theorem INVMN1: :: ZMODLAT3:20
for n being Nat
for M being Matrix of n,F_Real
for H being Matrix of n,F_Rat st M = H & M is invertible holds
( H is invertible & M ~ = H ~ )
proof end;

theorem INVMN2: :: ZMODLAT3:21
for n being Nat
for M being Matrix of n,F_Real st M is Matrix of n,F_Rat & M is invertible holds
M ~ is Matrix of n,F_Rat
proof end;

theorem ThGM3: :: ZMODLAT3:22
for L being non trivial positive-definite RATional Z_Lattice
for b being OrdBasis of L holds () ~ is Matrix of dim L,F_Rat
proof end;

theorem LmDE311A: :: ZMODLAT3:23
for X being finite Subset of RAT ex a being Element of INT st
( a <> 0 & ( for r being Element of RAT st r in X holds
a * r in INT ) )
proof end;

theorem LmDE311: :: ZMODLAT3:24
for L being non trivial positive-definite RATional Z_Lattice
for b being OrdBasis of L ex a being Element of F_Real st
( a is Element of INT.Ring & a <> 0 & a * (() ~) is Matrix of dim L,INT.Ring )
proof end;

LM0: for n being Nat
for F being FinSequence of F_Real st F = (Seg n) --> () holds
Sum F = 0. F_Real

proof end;

LM1: for L being Z_Lattice
for F, F0 being FinSequence of L
for l being Linear_Combination of L
for v being Vector of L st F is one-to-one & F0 is one-to-one & Carrier l c= rng F & canFS () = F0 holds
Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F0))

proof end;

theorem LmDE31: :: ZMODLAT3:25
for L being non trivial positive-definite RATional Z_Lattice
for b being OrdBasis of EMLat L
for i being Nat st i in dom b holds
ex v being Vector of () st
( () . ((b /. i),v) = 1 & ( for j being Nat st i <> j & j in dom b holds
() . ((b /. j),v) = 0 ) )
proof end;

LmDE00: for L being Z_Lattice
for v being Vector of () holds () . ((0. ()),v) in INT.Ring

proof end;

definition
let L be Z_Lattice;
mode Dual of L -> Vector of () means :defDualElement: :: ZMODLAT3:def 5
for v being Vector of () st v in EMbedding L holds
() . (it,v) in INT.Ring ;
existence
ex b1 being Vector of () st
for v being Vector of () st v in EMbedding L holds
() . (b1,v) in INT.Ring
proof end;
end;

:: deftheorem defDualElement defines Dual ZMODLAT3:def 5 :
for L being Z_Lattice
for b2 being Vector of () holds
( b2 is Dual of L iff for v being Vector of () st v in EMbedding L holds
() . (b2,v) in INT.Ring );

theorem LmDE0: :: ZMODLAT3:26
for L being Z_Lattice holds 0. () is Dual of L
proof end;

theorem LmDE1: :: ZMODLAT3:27
for L being Z_Lattice
for v, u being Dual of L holds v + u is Dual of L
proof end;

theorem LmDE2: :: ZMODLAT3:28
for L being Z_Lattice
for v being Dual of L
for a being Element of INT.Ring holds a * v is Dual of L
proof end;

definition
let L be Z_Lattice;
func DualSet L -> non empty Subset of () equals :: ZMODLAT3:def 6
{ v where v is Dual of L : verum } ;
correctness
coherence
{ v where v is Dual of L : verum } is non empty Subset of ()
;
proof end;
end;

:: deftheorem defines DualSet ZMODLAT3:def 6 :
for L being Z_Lattice holds DualSet L = { v where v is Dual of L : verum } ;

registration
let L be Z_Lattice;
coherence
proof end;
end;

definition
let L be Z_Lattice;
func DualLatMod L -> non empty strict LatticeStr over INT.Ring means :defDualMod: :: ZMODLAT3:def 7
( the carrier of it = DualSet L & the addF of it = the addF of () || () & the ZeroF of it = 0. () & the lmult of it = the lmult of () | [: the carrier of INT.Ring,():] & the scalar of it = () | [:(),():] );
existence
ex b1 being non empty strict LatticeStr over INT.Ring st
( the carrier of b1 = DualSet L & the addF of b1 = the addF of () || () & the ZeroF of b1 = 0. () & the lmult of b1 = the lmult of () | [: the carrier of INT.Ring,():] & the scalar of b1 = () | [:(),():] )
proof end;
uniqueness
for b1, b2 being non empty strict LatticeStr over INT.Ring st the carrier of b1 = DualSet L & the addF of b1 = the addF of () || () & the ZeroF of b1 = 0. () & the lmult of b1 = the lmult of () | [: the carrier of INT.Ring,():] & the scalar of b1 = () | [:(),():] & the carrier of b2 = DualSet L & the addF of b2 = the addF of () || () & the ZeroF of b2 = 0. () & the lmult of b2 = the lmult of () | [: the carrier of INT.Ring,():] & the scalar of b2 = () | [:(),():] holds
b1 = b2
;
end;

:: deftheorem defDualMod defines DualLatMod ZMODLAT3:def 7 :
for L being Z_Lattice
for b2 being non empty strict LatticeStr over INT.Ring holds
( b2 = DualLatMod L iff ( the carrier of b2 = DualSet L & the addF of b2 = the addF of () || () & the ZeroF of b2 = 0. () & the lmult of b2 = the lmult of () | [: the carrier of INT.Ring,():] & the scalar of b2 = () | [:(),():] ) );

theorem :: ZMODLAT3:29
for L being Z_Lattice holds DualLatMod L is Submodule of DivisibleMod L
proof end;

theorem LmDE21: :: ZMODLAT3:30
for L being Z_Lattice
for v being Vector of ()
for I being Basis of () st ( for u being Vector of () st u in I holds
() . (v,u) in INT.Ring ) holds
v is Dual of L
proof end;

definition
let L be positive-definite RATional Z_Lattice;
let I be Basis of ();
func DualBasis I -> Subset of () means :defDualBasis: :: ZMODLAT3:def 8
for v being Vector of () holds
( v in it iff ex u being Vector of () st
( u in I & () . (u,v) = 1 & ( for w being Vector of () st w in I & u <> w holds
() . (w,v) = 0 ) ) );
existence
ex b1 being Subset of () st
for v being Vector of () holds
( v in b1 iff ex u being Vector of () st
( u in I & () . (u,v) = 1 & ( for w being Vector of () st w in I & u <> w holds
() . (w,v) = 0 ) ) )
proof end;
uniqueness
for b1, b2 being Subset of () st ( for v being Vector of () holds
( v in b1 iff ex u being Vector of () st
( u in I & () . (u,v) = 1 & ( for w being Vector of () st w in I & u <> w holds
() . (w,v) = 0 ) ) ) ) & ( for v being Vector of () holds
( v in b2 iff ex u being Vector of () st
( u in I & () . (u,v) = 1 & ( for w being Vector of () st w in I & u <> w holds
() . (w,v) = 0 ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defDualBasis defines DualBasis ZMODLAT3:def 8 :
for L being positive-definite RATional Z_Lattice
for I being Basis of ()
for b3 being Subset of () holds
( b3 = DualBasis I iff for v being Vector of () holds
( v in b3 iff ex u being Vector of () st
( u in I & () . (u,v) = 1 & ( for w being Vector of () st w in I & u <> w holds
() . (w,v) = 0 ) ) ) );

definition
let L be positive-definite RATional Z_Lattice;
let I be Basis of ();
func B2DB I -> Function of I,() means :defB2DB: :: ZMODLAT3:def 9
( dom it = I & rng it = DualBasis I & ( for v being Vector of () st v in I holds
( () . (v,(it . v)) = 1 & ( for w being Vector of () st w in I & v <> w holds
() . (w,(it . v)) = 0 ) ) ) );
existence
ex b1 being Function of I,() st
( dom b1 = I & rng b1 = DualBasis I & ( for v being Vector of () st v in I holds
( () . (v,(b1 . v)) = 1 & ( for w being Vector of () st w in I & v <> w holds
() . (w,(b1 . v)) = 0 ) ) ) )
proof end;
uniqueness
for b1, b2 being Function of I,() st dom b1 = I & rng b1 = DualBasis I & ( for v being Vector of () st v in I holds
( () . (v,(b1 . v)) = 1 & ( for w being Vector of () st w in I & v <> w holds
() . (w,(b1 . v)) = 0 ) ) ) & dom b2 = I & rng b2 = DualBasis I & ( for v being Vector of () st v in I holds
( () . (v,(b2 . v)) = 1 & ( for w being Vector of () st w in I & v <> w holds
() . (w,(b2 . v)) = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defB2DB defines B2DB ZMODLAT3:def 9 :
for L being positive-definite RATional Z_Lattice
for I being Basis of ()
for b3 being Function of I,() holds
( b3 = B2DB I iff ( dom b3 = I & rng b3 = DualBasis I & ( for v being Vector of () st v in I holds
( () . (v,(b3 . v)) = 1 & ( for w being Vector of () st w in I & v <> w holds
() . (w,(b3 . v)) = 0 ) ) ) ) );

registration
let L be positive-definite RATional Z_Lattice;
let I be Basis of ();
correctness
coherence
( B2DB I is onto & B2DB I is one-to-one )
;
proof end;
end;

theorem ThDB1: :: ZMODLAT3:31
for L being positive-definite RATional Z_Lattice
for I being Basis of () holds card I = card ()
proof end;

registration
let L be positive-definite RATional Z_Lattice;
let I be Basis of ();
correctness
coherence ;
proof end;
end;

registration
let L be non trivial positive-definite RATional Z_Lattice;
let I be Basis of ();
cluster DualBasis I -> non empty ;
correctness
coherence
not DualBasis I is empty
;
proof end;
end;

theorem LmDE32: :: ZMODLAT3:32
for L being positive-definite RATional Z_Lattice
for I being Basis of ()
for v being Vector of ()
for l being Linear_Combination of DualBasis I st v in I holds
() . (v,(Sum l)) = l . ((B2DB I) . v)
proof end;

theorem ThDE3: :: ZMODLAT3:33
for L being positive-definite RATional Z_Lattice
for I being Basis of ()
for v being Vector of () st v is Dual of L holds
v in Lin ()
proof end;

registration
let L be positive-definite RATional Z_Lattice;
let I be Basis of ();
correctness
proof end;
end;

definition
let L be positive-definite RATional Z_Lattice;
func DualLat L -> strict Z_Lattice means :defDualLat: :: ZMODLAT3:def 10
( the carrier of it = DualSet L & 0. it = 0. () & the addF of it = the addF of () || the carrier of it & the lmult of it = the lmult of () | [: the carrier of INT.Ring, the carrier of it:] & the scalar of it = () || the carrier of it );
existence
ex b1 being strict Z_Lattice st
( the carrier of b1 = DualSet L & 0. b1 = 0. () & the addF of b1 = the addF of () || the carrier of b1 & the lmult of b1 = the lmult of () | [: the carrier of INT.Ring, the carrier of b1:] & the scalar of b1 = () || the carrier of b1 )
proof end;
uniqueness
for b1, b2 being strict Z_Lattice st the carrier of b1 = DualSet L & 0. b1 = 0. () & the addF of b1 = the addF of () || the carrier of b1 & the lmult of b1 = the lmult of () | [: the carrier of INT.Ring, the carrier of b1:] & the scalar of b1 = () || the carrier of b1 & the carrier of b2 = DualSet L & 0. b2 = 0. () & the addF of b2 = the addF of () || the carrier of b2 & the lmult of b2 = the lmult of () | [: the carrier of INT.Ring, the carrier of b2:] & the scalar of b2 = () || the carrier of b2 holds
b1 = b2
;
end;

:: deftheorem defDualLat defines DualLat ZMODLAT3:def 10 :
for L being positive-definite RATional Z_Lattice
for b2 being strict Z_Lattice holds
( b2 = DualLat L iff ( the carrier of b2 = DualSet L & 0. b2 = 0. () & the addF of b2 = the addF of () || the carrier of b2 & the lmult of b2 = the lmult of () | [: the carrier of INT.Ring, the carrier of b2:] & the scalar of b2 = () || the carrier of b2 ) );

theorem ThDL1: :: ZMODLAT3:34
for L being positive-definite RATional Z_Lattice
for v being Vector of () holds
( v in DualLat L iff v is Dual of L )
proof end;

theorem ThDL2: :: ZMODLAT3:35
for L being positive-definite RATional Z_Lattice holds DualLat L is Submodule of DivisibleMod L
proof end;

theorem ThELEM1: :: ZMODLAT3:36
for L being Z_Lattice
for I being Basis of () holds I is Basis of ()
proof end;

theorem :: ZMODLAT3:37
for L being Z_Lattice
for I being Basis of () holds I is Basis of ()
proof end;

theorem ThDB2: :: ZMODLAT3:38
for L being positive-definite RATional Z_Lattice
for I being Basis of ()
for v being Vector of () st v in DualBasis I holds
v is Dual of L
proof end;

theorem ThDLDB: :: ZMODLAT3:39
for L being positive-definite RATional Z_Lattice
for I being Basis of () holds DualBasis I is Basis of ()
proof end;

theorem :: ZMODLAT3:40
for L being positive-definite RATional Z_Lattice
for b being OrdBasis of EMLat L
for I being Basis of () st I = rng b holds
(B2DB I) * b is OrdBasis of DualLat L
proof end;

theorem LmEMDetX3: :: ZMODLAT3:41
for L being positive-definite Z_Lattice
for b being OrdBasis of L
for e being OrdBasis of EMLat L st e = () * b holds
GramMatrix ((),b) = GramMatrix ((),e)
proof end;

theorem :: ZMODLAT3:42
for L being positive-definite Z_Lattice holds GramDet () = GramDet ()
proof end;

theorem ThRankDL: :: ZMODLAT3:43
for L being positive-definite RATional Z_Lattice holds rank L = rank ()
proof end;

theorem :: ZMODLAT3:44
for L being INTegral positive-definite Z_Lattice holds EMLat L is Z_Sublattice of DualLat L
proof end;

theorem :: ZMODLAT3:45
for L being Z_Lattice
for b being OrdBasis of L st GramMatrix ((),b) is Matrix of dim L,INT.Ring holds
L is INTegral
proof end;

theorem ThRatLat1B: :: ZMODLAT3:46
for L being Z_Lattice
for I being finite Subset of L
for u being Vector of L st ( for v being Vector of L st v in I holds
<;v,u;> in RAT ) holds
for v being Vector of L st v in Lin I holds
<;v,u;> in RAT
proof end;

theorem ThRatLat1A: :: ZMODLAT3:47
for L being Z_Lattice
for I being Basis of L st ( for v, u being Vector of L st v in I & u in I holds
<;v,u;> in RAT ) holds
for v, u being Vector of L holds <;v,u;> in RAT
proof end;

theorem ThRatLat1: :: ZMODLAT3:48
for L being Z_Lattice
for I being Basis of L st ( for v, u being Vector of L st v in I & u in I holds
<;v,u;> in RAT ) holds
L is RATional
proof end;

theorem :: ZMODLAT3:49
for L being Z_Lattice
for b being OrdBasis of L st GramMatrix ((),b) is Matrix of dim L,F_Rat holds
L is RATional
proof end;

registration
let L be positive-definite RATional Z_Lattice;
correctness
coherence ;
proof end;
end;

theorem ThSLGM2: :: ZMODLAT3:50
for L being RATional Z_Lattice
for LX being Z_Lattice
for b being OrdBasis of LX st LX is Submodule of DivisibleMod L & the scalar of LX = () || the carrier of LX holds
GramMatrix ((),b) is Matrix of dim LX,F_Rat
proof end;

theorem :: ZMODLAT3:51
for L being positive-definite RATional Z_Lattice
for b being OrdBasis of DualLat L holds GramMatrix ((),b) is Matrix of dim L,F_Rat
proof end;

theorem ThSLGM3: :: ZMODLAT3:52
for L being positive-definite Z_Lattice
for LX being Z_Lattice st LX is Submodule of DivisibleMod L & the scalar of LX = () || the carrier of LX holds
LX is positive-definite
proof end;

registration
let L be positive-definite RATional Z_Lattice;
correctness
proof end;
end;

registration
let L be non trivial positive-definite RATional Z_Lattice;
cluster DualLat L -> non trivial strict ;
correctness
coherence
not DualLat L is trivial
;
proof end;
end;