<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

Data publikacji: 31 sie 2016

Zakres stron: 49 - 68

Otrzymano: 30 gru 2015

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

Słowa kluczowe
ℤ-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

Data publikacji: 31 sie 2016

Zakres stron: 49 - 68

Otrzymano: 30 gru 2015

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

Słowa kluczoweℤ-lattice, Gram matrix, integral ℤ-lattice, positive definite ℤ-lattice

© by Yuichi Futa

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

Słowa kluczowe
ℤ-lattice, Gram matrix, integral ℤ-lattice, positive definite ℤ-lattice