# Embedded Lattice and Properties of Gram Matrix

Formalized Mathematics (2017)

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

## Access Full Article

top## Abstract

top## How to cite

topYuichi 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 ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.