<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

Publié en ligne: 31 août 2016

Pages: 49 - 68

Reçu: 30 déc. 2015

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

Mots clés
ℤ-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

Publié en ligne: 31 août 2016

Pages: 49 - 68

Reçu: 30 déc. 2015

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

Mots clésℤ-lattice, Gram matrix, integral ℤ-lattice, positive definite ℤ-lattice

© by Yuichi Futa

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

Mots clés
ℤ-lattice, Gram matrix, integral ℤ-lattice, positive definite ℤ-lattice