Gaussian Integers

Yuichi Futa; Hiroyuki Okazaki; Daichi Mizushima; Yasunari Shidama

doi:10.2478/forma-2013-0013

.blurhash-client-img { display: none !important; }

Gaussian Integers

Formalized Mathematics

Volume 21 (2013): Issue 2 (June 2013)

By: Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima and Yasunari Shidama

Open Access

|Jun 2013

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.

References

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.
Search in Google Scholar
[2] Grzegorz Bancerek. Konig’s theorem. Formalized Mathematics, 1(3):589-593, 1990.
Search in Google Scholar
[3] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.
Search in Google Scholar
[4] Józef Białas. Group and field definitions. Formalized Mathematics, 1(3):433-439, 1990.
Search in Google Scholar
[5] Czesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180, 1990.
Search in Google Scholar
[6] Czesław Bylinski. The complex numbers. Formalized Mathematics, 1(3):507-513, 1990.
Search in Google Scholar
[7] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.
Search in Google Scholar
[8] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
Search in Google Scholar
[9] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.
Search in Google Scholar
[10] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
Search in Google Scholar
[11] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.
Search in Google Scholar
[12] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Set of points on elliptic curve in projective coordinates. Formalized Mathematics, 19(3):131-138, 2011. doi:10.2478/v10037-011-0021-6.10.2478/v10037-011-0021-6
Search in Google Scholar
[13] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Z-modules. Formalized Mathematics, 20(1):47-59, 2012. doi:10.2478/v10037-012-0007-z.10.2478/v10037-012-0007-z
Search in Google Scholar
[14] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841-845, 1990.
Search in Google Scholar
[15] Eugeniusz Kusak, Wojciech Leonczuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990.
Search in Google Scholar
[16] Rafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Formalized Mathematics, 1(5):829-832, 1990.
Search in Google Scholar
[17] Michał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3-11, 1991.
Search in Google Scholar
[18] Christoph Schwarzweller. The correctness of the generic algorithms of Brown and Henrici concerning addition and multiplication in fraction fields. Formalized Mathematics, 6(3): 381-388, 1997.
Search in Google Scholar
[19] Christoph Schwarzweller. The ring of integers, Euclidean rings and modulo integers. Formalized Mathematics, 8(1):29-34, 1999.
Search in Google Scholar
[20] Christoph Schwarzweller. The field of quotients over an integral domain. Formalized Mathematics, 7(1):69-79, 1998.
Search in Google Scholar
[21] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4): 341-347, 2003.
Search in Google Scholar
[22] Andrzej Trybulec and Czesław Bylinski. Some properties of real numbers. Formalized Mathematics, 1(3):445-449, 1990.
Search in Google Scholar
[23] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.
Search in Google Scholar
[24] Wojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821-827, 1990.
Search in Google Scholar
[25] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.
Search in Google Scholar
[26] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
Search in Google Scholar
[27] Andr´e Weil. Number Theory for Beginners. Springer-Verlag, 1979.10.1007/978-1-4612-9957-8
Search in Google Scholar
[28] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.
Search in Google Scholar

Articles in this issue

DOI: https://doi.org/10.2478/forma-2013-0013 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630

Journal RSS Feed

Language: English

Page range: 115 - 125

Published on: Jun 1, 2013

Published by: University of Białystok

In partnership with: Paradigm Publishing Services

Publication frequency: 1 issue per year

Keywords:

formalization of Gaussian integers,

algebraic integers

Related subjects:

Mathematics,

Logic and set theory,

Computer sciences,

Artificial intelligence

© 2013 Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima, Yasunari Shidama, published by University of Białystok
This work is licensed under the Creative Commons License.

Volume 21 (2013): Issue 2 (June 2013)