Formalization of Gaussian integers, Gaussian rational numbers, and their algebraic structures with Mizar

In this paper, we introduce formal definitions and theorems in the Mizar proof checking system for the Gaussian integer ring and the Z-module constructed from Gaussian integers, as well as for Gaussian rational numbers and the Gaussian rational field. We then prove that the Gaussian rational field and the quotient field of the Gaussian integer ring are isomorphic. We prove the correctness of our formalization by using the Mizar proof checking system as a formal verification tool.