<abstract xmlns="http://www.w3.org/1999/xhtml"><p> In this article, we formalize the definition of lattice of ℤ-module and its properties in the Mizar system [5].We formally prove that scalar products in lattices are bilinear forms over the field of real numbers ℝ. We also formalize the definitions of positive definite and integral lattices and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [14], and cryptographic systems with lattices [15] and coding theory [9].</p></abstract>

In this article, we formalize the definition of lattice of ℤ-module and its properties in the Mizar system [5].We formally prove that scalar products in lattices are bilinear forms over the field of real numbers ℝ. We also formalize the definitions of positive definite and integral lattices and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [14], and cryptographic systems with lattices [15] and coding theory [9].

Lattice of ℤ-module

Japan Advanced Institute of Science and Technology Ishikawa, Japan

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

{"article-title":"Lattice of ℤ-module"}

In this article, we formalize the definition of lattice of ℤ-module and its properties in the Mizar system [5].We formally prove that scalar products in...

Lattice of ℤ-module

Published Online: Aug 31, 2016

Page range: 49 - 68

Received: Dec 30, 2015

DOI: https://doi.org/10.1515/forma-2016-0005

Keywords
ℤ-lattice, Gram matrix, integral ℤ-lattice, positive definite ℤ-lattice

© by Yuichi Futa

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Lattice of ℤ-module

Published Online: Aug 31, 2016

Page range: 49 - 68

Received: Dec 30, 2015

DOI: https://doi.org/10.1515/forma-2016-0005

Keywordsℤ-lattice, Gram matrix, integral ℤ-lattice, positive definite ℤ-lattice

© by Yuichi Futa

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Keywords
ℤ-lattice, Gram matrix, integral ℤ-lattice, positive definite ℤ-lattice