@MISC{ZMODLAT3.MIZ,
  AUTHOR = {Futa, Yuichi and Shidama, Yasunari},
  TITLE = {Dual Lattice of $\mathbb Z$-module Lattice},
  SECTION1 = {Summation of Inner Products},
  SECTION2 = {Dual Lattice},
  DAY = {27},
  MONTH = {June},
  YEAR = {2017},
  ADDRESS1 = {Tokyo University of Technology, Tokyo, JAPAN},
  ADDRESS2 = {Shinshu University, Nagano, JAPAN},
  SUMMARY = {In this article, we formalize the definition of
  dual lattice and their properties.
  We formally prove that a set of all dual vectors in a rational lattice
  has the construction of a lattice.  
  We show that a dual basis can be calculated by elements of an inverse 
  of the Gram Matrix.
  We also formalize a summation of inner products and its properties.
  Lattice of $\mathbb Z$-module is necessary for lattice problems,
  LLL(Lenstra, Lenstra and Lov\'asz) base reduction algorithm
  and cryptographic systems with lattice \cite{LAT}.},
  NOTE = {This work was supported by JSPS KAKENHI 15K00183.}}

@ARTICLE(LAT,
      AUTHOR  = {Daniele Micciancio and Shafi Goldwasser},
      TITLE   = {Complexity of Lattice Problems:
      A Cryptographic Perspective (The International Series
      in Engineering and Computer Science)},
      PUBLISHER={Springer},
      YEAR    = 2002)
