Embedded Lattice and Properties of Gram Matrix

• Autorzy: Yuichi Futa , Yasunari Shidama
• Języki publikacji: EN

Abstrakty

EN

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

Słowa kluczowe

EN

Z-lattice; Gram matrix; rational Z-lattice

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2017
• Tom: 25
• Numer: 1
• Strony: 73-86

Daty

wydano

2017-03-28

otrzymano

2017-03-17

online

2017-05-11

Twórcy

autor

Yuichi Futa

• , ,

autor

Yasunari Shidama

• , ,

Identyfikatory

DOI

10.1515/forma-2017-0007