Dual Lattice of ℤ-module Lattice

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

Abstrakty

EN

In this article, we formalize in Mizar [5] the definition of dual lattice and their properties. We formally prove that a set of all dual vectors in a rational lattice has the construction of a lattice. We show that a dual basis can be calculated by elements of an inverse of the Gram Matrix. We also formalize a summation of inner products and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems with lattice [20], [10] and [19].

Słowa kluczowe

EN

ℤ-lattice; dual lattice of ℤ-lattice; dual basis of ℤ-lattice

Kategorie tematyczne

• 03B35: Mechanization of proofs and logical operations
• 15A09: Matrix inversion, generalized inverses
• 15A03: Vector spaces, linear dependence, rank

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2017
• Tom: 25
• Numer: 2
• Strony: 157-169

Daty

wydano

2017-07-01

otrzymano

2017-06-27

online

2017-09-23

Twórcy

autor

Yuichi Futa

• , ,

autor

Yasunari Shidama

• , ,

Identyfikatory

DOI

10.1515/forma-2017-0015