@article{oai:soar-ir.repo.nii.ac.jp:00018383, author = {Futa, Yuichi and Okazaki, Hiroyuki and Shidama, Yasunari}, issue = {4}, journal = {Formalized Mathematics}, month = {Dec}, note = {Article, Formalized Mathematics. 21(4): 273-282 (2013)}, pages = {273--282}, title = {Submodule of free Z-module}, volume = {21}, year = {2013} }