:: deftheorem defScProductEM defines ScProductEM ZMODLAT2:def 2 :
for L being Z_Lattice
for b₂ being Function of [: the carrier of (EMbedding L), the carrier of (EMbedding L):], the carrier of F_Real holds
( b₂ = ScProductEM L iff for v, u being Vector of L
for vv, uu being Vector of (EMbedding L) st vv = (MorphsZQ L) . v & uu = (MorphsZQ L) . u holds
b₂ . (vv,uu) = <;v,u;> );