Dual Lattice of ℤ-module Lattice

Yuichi 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 -