@MISC{VECTSP12.MIZ,
  AUTHOR = {Futa, Yuichi and Shidama, Yasunari},
  TITLE = {Isomorphism Theorem on Vector Spaces over a Ring},
  SECTION1 = {Bijective Linear Transformation},
  SECTION2 = {Properties of Linear Combinations of Modules over a Ring},
  SECTION3 = {1st Isomophism Theorem},
  SECTION4 = {The Product Space of Vector Spaces},
  SECTION5 = {Cartesian Product of Vector Spaces},
  DAY = {30},
  MONTH = {August},
  YEAR = {2017},
  ADDRESS1 = {Tokyo University of Technology, Tokyo, Japan},
  ADDRESS2 = {Shinshu University, Nagano, Japan},
  SUMMARY = {In this article, we formalize some properties on vector spaces
  over a ring.  We formally prove the 1st isomorphism theorem on vector spaces
  over a ring.
  We also formalize the product space of vector spaces.
  $\mathbb Z$-module is necessary for lattice problems,
  LLL (Lenstra, Lenstra and Lov\'asz) base reduction algorithm
  and cryptographic systems with lattice \cite{LAT}.
  Some theorems in this article are described by translating
  theorems in \cite{RANKNULL.ABS}, \cite{ZMODUL05.ABS},
  and \cite{ZMODUL07.ABS}
  into theorems of vector spaces over a ring.},
  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)
