Embedded Lattice and Properties of Gram Matrix

Yuichi Futa; Yasunari Shidama

Formalized Mathematics (2017)

  • Volume: 25, Issue: 1, page 73-86
  • ISSN: 1426-2630

Abstract

top
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].

How to cite

top

Yuichi Futa, and Yasunari Shidama. "Embedded Lattice and Properties of Gram Matrix." Formalized Mathematics 25.1 (2017): 73-86. <http://eudml.org/doc/288150>.

@article{YuichiFuta2017,
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].},
author = {Yuichi Futa, Yasunari Shidama},
journal = {Formalized Mathematics},
keywords = {Z-lattice; Gram matrix; rational Z-lattice; $\mathbb \{Z\}$-lattice; rational $\mathbb \{Z\}$-lattice},
language = {eng},
number = {1},
pages = {73-86},
title = {Embedded Lattice and Properties of Gram Matrix},
url = {http://eudml.org/doc/288150},
volume = {25},
year = {2017},
}

TY - JOUR
AU - Yuichi Futa
AU - Yasunari Shidama
TI - Embedded Lattice and Properties of Gram Matrix
JO - Formalized Mathematics
PY - 2017
VL - 25
IS - 1
SP - 73
EP - 86
AB - 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].
LA - eng
KW - Z-lattice; Gram matrix; rational Z-lattice; $\mathbb {Z}$-lattice; rational $\mathbb {Z}$-lattice
UR - http://eudml.org/doc/288150
ER -

NotesEmbed ?

top

You must be logged in to post comments.