<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

Pubblicato online: 31 ago 2016

Pagine: 49 - 68

Ricevuto: 30 dic 2015

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

Parole chiave
ℤ-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

Pubblicato online: 31 ago 2016

Pagine: 49 - 68

Ricevuto: 30 dic 2015

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

Parole chiaveℤ-lattice, Gram matrix, integral ℤ-lattice, positive definite ℤ-lattice

© by Yuichi Futa

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

Parole chiave
ℤ-lattice, Gram matrix, integral ℤ-lattice, positive definite ℤ-lattice