:: deftheorem defScProductDM defines ScProductDM ZMODLAT2:def 3 :
for L being Z_Lattice
for b₂ being Function of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):], the carrier of F_Real holds
( b₂ = ScProductDM L iff for vv, uu being Vector of (DivisibleMod L)
for v, u being Vector of (EMbedding L)
for a, b being Element of INT.Ring
for ai, bi being Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu holds
b₂ . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) );