@ARTICLE{ZMODLAT2.MIZ,
  AUTHOR = {Futa, Yuichi and Shidama, Yasunari},
  TITLE = {Embedded Lattice and Properties of {G}ram Matrix},
  SECTION1 = {Inner Product of Embedded Module},
  SECTION2 = {Embedding of Lattice}
  SECTION3 = {Properties of Gram Matrix},
  DAY = {17},
  MONTH = {March},
  YEAR = {2017},
  ADDRESS1 = {Tokyo University of Technology, Tokyo, JAPAN},
  ADDRESS2 = {Shinshu University, Nagano, JAPAN},
  SUMMARY = {In this article, we formalize the definition of
  embedding of lattice and its properties.
  We formally define an inner product on an embedded module.
  We also formalize properties of Gram matrix.
  We formally prove that an inverse of Gram matrix for a rational lattice
  exists.
  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)
