@MISC{ZMODUL06.MIZ,
  AUTHOR = {Futa, Yuichi and Okazaki, Hiroyuki and Nakasho, Kazuhisa and Shidama, Yasunari},
  TITLE = {Torsion $\mathbb Z$-module and Torsion-free $\mathbb Z$-module},
  SECTION1 = {Torsion $\mathbb{Z}$-module and Torsion-free $\mathbb{Z}$-module},
  SECTION2 = {Rank of Finite-rank Free $\mathbb{Z}$-module},
  DAY = {29},
  MONTH = {November},
  YEAR = {2014},
  ADDRESS2 = {Japan Advanced Institute of Science and Technology, Ishikawa, Japan},
  ADDRESS2 = {Shinshu University, Nagano, Japan},
  ADDRESS3 = {Shinshu University, Nagano, Japan},
  ADDRESS4 = {Shinshu University, Nagano, Japan},
  SUMMARY = {In this article, we formalize a torsion $\mathbb Z$-module and
  a torsion-free $\mathbb Z$-module.  Especially, we prove formally that
  finitely-generated torsion-free $\mathbb Z$-modules are finite-rank free.
  We also formalize properties related to rank of finite-rank free
  $\mathbb Z$-modules.
  The notion of $\mathbb Z$-module is necessary for solving
  lattice problems,
  LLL (Lenstra, Lenstra, and Lov\'asz) base reduction algorithm
  and cryptographic systems over lattices \cite{LAT}.},
  ACKNOWLEDGEMENT = {This work was supported by JSPS
     KAKENHI 21240001 and 22300285.}}

@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)
