@article{oai:soar-ir.repo.nii.ac.jp:00018397, author = {Futa, Yuichi and Okazaki, Hiroyuki and Shidama, Yasunari}, issue = {1}, journal = {Formalized Mathematics}, month = {Jan}, note = {Article, Formalized Mathematics. 20(1): 47-59 (2012)}, pages = {47--59}, title = {Z-modules}, volume = {20}, year = {2012} }