<abstract xmlns="http://www.w3.org/1999/xhtml"><p>Gaussian integer is one of basic algebraic integers. In this article we formalize some definitions about Gaussian integers [27]. 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.</p></abstract>

Gaussian integer is one of basic algebraic integers. In this article we formalize some definitions about Gaussian integers [27]. 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.

Gaussian Integers

Japan Advanced Institute of Science and Technology Ishikawa, Japan

This research was presented during the 2012 International Symposium on Information
Theory and its Applications (ISITA2012) in Honolulu, USA.

This work was supported by JSPS KAKENHI 21240001 and 22300285.

Formalized Mathematics

{"subtitle":{"sup":"*"},"article-title":"Gaussian Integers"}

Gaussian integer is one of basic algebraic integers. In this article we formalize some definitions about Gaussian integers [27]. We also formalize ring (called...

Gaussian Integers

Published Online: Jun 01, 2013

Page range: 115 - 125

DOI: https://doi.org/10.2478/forma-2013-0013

Keywords
formalization of Gaussian integers, algebraic integers

This content is open access.

Gaussian Integers

Published Online: Jun 01, 2013

Page range: 115 - 125

DOI: https://doi.org/10.2478/forma-2013-0013

Keywordsformalization of Gaussian integers, algebraic integers

This content is open access.

Keywords
formalization of Gaussian integers, algebraic integers