<abstract xmlns="http://www.w3.org/1999/xhtml"><p> In this article, we formalize in Mizar [14] the definition of embedding of lattice and its properties. We formally define an inner product on an embedded module. We also formalize properties of Gram matrix. We formally prove that an inverse of Gram matrix for a rational lattice exists. Lattice of Z-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lov´asz) base reduction algorithm [16] and cryptographic systems with lattice [17].</p></abstract>

In this article, we formalize in Mizar [14] the definition of embedding of lattice and its properties. We formally define an inner product on an embedded module. We also formalize properties of Gram matrix. We formally prove that an inverse of Gram matrix for a rational lattice exists. Lattice of Z-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lov´asz) base reduction algorithm [16] and cryptographic systems with lattice [17].

Embedded Lattice and Properties of Gram Matrix

Formalized Mathematics

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

{"article-title":"Embedded Lattice and Properties of Gram Matrix"}

In this article, we formalize in Mizar [14] the definition of embedding of lattice and its properties. We formally define an inner product on an embedded...

Embedded Lattice and Properties of Gram Matrix

Online veröffentlicht: 11. Mai 2017

Seitenbereich: 73 - 86

Eingereicht: 17. März 2017

DOI: https://doi.org/10.1515/forma-2017-0007

Schlüsselwörter
Z-lattice, Gram matrix, rational Z-lattice

© by Yuichi Futa

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

Embedded Lattice and Properties of Gram Matrix

Online veröffentlicht: 11. Mai 2017

Seitenbereich: 73 - 86

Eingereicht: 17. März 2017

DOI: https://doi.org/10.1515/forma-2017-0007

SchlüsselwörterZ-lattice, Gram matrix, rational Z-lattice

© by Yuichi Futa

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

Schlüsselwörter
Z-lattice, Gram matrix, rational Z-lattice