# Dual Lattice of ℤ-module Lattice

Formalized Mathematics (2017)

- Volume: 25, Issue: 2, page 157-169
- ISSN: 1426-2630

## Access Full Article

top## Abstract

top## How to cite

topYuichi Futa, and Yasunari Shidama. "Dual Lattice of ℤ-module Lattice." Formalized Mathematics 25.2 (2017): 157-169. <http://eudml.org/doc/288317>.

@article{YuichiFuta2017,

abstract = {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].},

author = {Yuichi Futa, Yasunari Shidama},

journal = {Formalized Mathematics},

keywords = {ℤ-lattice; dual lattice of ℤ-lattice; dual basis of ℤ-lattice},

language = {eng},

number = {2},

pages = {157-169},

title = {Dual Lattice of ℤ-module Lattice},

url = {http://eudml.org/doc/288317},

volume = {25},

year = {2017},

}

TY - JOUR

AU - Yuichi Futa

AU - Yasunari Shidama

TI - Dual Lattice of ℤ-module Lattice

JO - Formalized Mathematics

PY - 2017

VL - 25

IS - 2

SP - 157

EP - 169

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

LA - eng

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

UR - http://eudml.org/doc/288317

ER -

## NotesEmbed ?

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