@MISC{GAUSSINT.MIZ,
  AUTHOR = {Futa, Yuichi and Okazaki, Hiroyuki and Mizushima, Daichi and Shidama, Yasunari},
  TITLE = {Gaussian Integers},
  SECTION1 = {Gaussian Integer Ring},
  SECTION2 = {$\mathbb Z$-Algebra},
  SECTION3 = {Denumerable Set},
  SECTION4 = {Quotient Field of Gaussian Integer Ring},
  SECTION5 = {Rational Field},
  SECTION6 = {Gaussian Rational Number Field},
  SECTION7 = {Gaussian Integer Ring is Euclidian},
  DAY = {19},
  MONTH = {May},
  YEAR = {2013},
  ADDRESS1 = {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 = {Gaussian integer is one of basic algebraic integers.
  In this article, we formalize some definitions about Gaussian integers
  \cite{Weil79}.
  We also formalize ring (called Gaussian integer ring), Z-module and
  Z-algebra generated by Gaussian integer mentioned above.
  Moreover, we formalize some definitions about Gaussian rational
  numbers and Gaussian rational number field.
  Then we prove that the Gaussian rational number field and a quotient field
  of the Gaussian integer ring are isomorphic.},
  ACKNOWLEDGEMENT = {This work was supported by JSPS
  KAKENHI 21240001 and 22300285.}}

@BOOK{Weil79,
      AUTHOR = {Weil, Andr\'e},
      TITLE = {Number Theory for Beginners},
      PUBLISHER = {Springer-Verlag},
      YEAR = {1979}}
