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].
Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
Daniele Micciancio and Shafi Goldwasser. Complexity of lattice problems: A cryptographic perspective (the international series in engineering and computer science). 2002.
Christoph Schwarzweller. The binomial theorem for algebraic structures. Formalized Mathematics, 9(3):559-564, 2001.
Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115-122, 1990.
Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97-105, 1990.
Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.
Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.
Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990.
Stanisław Żukowski. Introduction to lattice theory. Formalized Mathematics, 1(1):215-222, 1990.