@MISC{ZMATRLIN.MIZ,
  AUTHOR = {Futa, Yuichi and Okazaki, Hiroyuki and Shidama, Yasunari},
  TITLE = {Matrix of $\mathbb Z$-module},
  SECTION1 = {Preliminaries},
  SECTION2 = {Sequences and Matrices Concerning Linear Transformations},
  SECTION3 = {Decomposition of a Vector in Basis},
  SECTION4 = {Matrices of Linear Transformations},
  SECTION5 = {Real-valued Function of $\mathbb Z$-Module},
  SECTION6 = {Bilinear form of $\mathbb Z$-Module},
  SECTION7 = {Matrix of Bilinear Form},
  DAY = {18},
  MONTH = {February},
  YEAR = {2015},
  ADDRESS1 = {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 a matrix of $\mathbb Z$-module and
  its properties.  Specially, we formalize a matrix of a linear transformation
  of $\mathbb Z$-module, a bilinear form and a matrix of the bilinear form
  (Gramian matrix).  We formally prove that for a finite-rank free
  $\mathbb Z$-module $V$, determinant of its Gramian matrix is constant
  regardless of selection of its basis.
  $\mathbb Z$-module is necessary for lattice problems,
  LLL (Lenstra, Lenstra and Lov\'asz) base reduction algorithm
  and cryptographic systems with lattices \cite{LAT}.
  Some theorems in this article are described by translating
  theorems in \cite{MATRLIN.ABS}, \cite{HAHNBAN.ABS} and \cite{BILINEAR.ABS}
  into theorems of $\mathbb Z$-module.},
  NOTE = {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)
