@MISC{ZMODUL08.MIZ,
  AUTHOR = {Futa, Yuichi and Shidama, Yasunari},
  TITLE = {Divisible $\mathbb Z$-modules},
  SECTION1 = {Divisible Module},
  SECTION2 = {Divisible Module for Torsion-free $\mathbb Z$-module},
  DAY = {30},
  MONTH = {December},
  YEAR = {2015},
  ADDRESS2 = {Japan Advanced Institute of Science and Technology, Ishikawa, JAPAN},
  ADDRESS2 = {Shinshu University, Nagano, JAPAN},
  SUMMARY = {In this article, we formalize the definition of divisible
  $\mathbb Z$-module and its properties in the Mizar system \cite{Mizar:2015}.
  We formally prove that any non-trivial divisible $\mathbb Z$-modules are
  not finitely-generated.
  We introduce a divisible $\mathbb Z$-module, equivalent to
  a vector space of a torsion-free $\mathbb Z$-module
  with a coefficient ring $\mathbb Q$.
  $\mathbb Z$-modules are important for lattice problems,
  LLL (Lenstra, Lenstra and Lov\'asz) base reduction algorithm \cite{LLL:1982},
  cryptographic systems with lattices \cite{Micciancio:2002}
  and coding theory \cite{Ebeling:2013}.}}

@inproceedings{Mizar:2015,
  author    = {Bancerek, Grzegorz and
               Byli{\'n}ski, Czes{\l}aw and
               Grabowski, Adam and
               Korni{\l}owicz, Artur and
               Matuszewski, Roman and
               Naumowicz, Adam and
               P\c{a}k, Karol and
               Urban, Josef},
  title     = {Mizar: State-of-the-art and Beyond},
  booktitle = {Intelligent Computer Mathematics -- International Conference,
               {CICM} 2015, Washington, DC, USA, July 13--17, 2015, Proceedings},
  pages     = {261--279},
  year      = {2015},
  crossref  = {DBLP:conf/mkm/2015},
  url       = {http://dx.doi.org/10.1007/978-3-319-20615-8_17},
  doi       = {10.1007/978-3-319-20615-8_17}}

@ARTICLE{LLL:1982,
      AUTHOR  = {A. K. Lenstra, H. W. Lenstra Jr. and L. Lov\'{a}sz},
      TITLE   = {Factoring polynomials with rational coefficients},
      PUBLISHER={Springer-Verlag},
      SERIES = {Mathematische Annalen},
      VOLUME = {261},
      NUMBER = {4},
      YEAR    = {1982}}

@ARTICLE{Micciancio:2002,
      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}}

@BOOK{Ebeling:2013,
      AUTHOR  = {Wolfgang Ebeling},
      TITLE   = {Lattices and Codes},
      PUBLISHER={Springer Fachmedien Wiesbaden},
      SERIES = {Advanced Lectures in Mathematics},
      YEAR    = {2013}}
