Z-modules Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama (2012) Formalized Mathematics In this article, we formalize Z-module, that is a module over integer ring. Z-module is necassary for lattice problems, LLL (Lenstra-Lenstra-Lovász) base reduction algorithm and cryptographic systems with lattices [11].