@MISC{ZMODUL07.MIZ,
  AUTHOR = {Futa, Yuichi and Okazaki, Hiroyuki and Shidama, Yasunari},
  TITLE = {Torsion-part of $\mathbb Z$-module},
  SECTION1 = {Torsion-part of $\mathbb{Z}$-module},
  SECTION2 = {$\mathbb Z$-module Generated by the Field of Rational Numbers},
  SECTION3 = {The Rank-nullity Theorem},
  DAY = {14},
  MONTH = {August},
  YEAR = {2015},
  ADDRESS2 = {Japan Advanced Institute of Science and Technology, Ishikawa, Japan},
  ADDRESS2 = {Shinshu University, Nagano, Japan},
  ADDRESS3 = {Shinshu University, Nagano, Japan},
  SUMMARY = {In this article, we formalize the definition of "torsion-part"
  of $\mathbb Z$-module and its properties.
  We show $\mathbb Z$-module generated by the field of rational numbers
  as an example of torsion-free non free $\mathbb Z$-modules.
  We also formalize the rank-nullity theorem over finite-rank free
  $\mathbb Z$-modules.
  $\mathbb Z$-module is necessary for lattice problems,
  LLL (Lenstra, Lenstra and Lov\'asz) base reduction algorithm
  and cryptographic systems with lattices \cite{LAT}.}}

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