Z-modules
Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama · Formalized Mathematics · 2012
Z-modulesIn 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].