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].
@article{bwmeta1.element.doi-10_1515_forma-2017-0015,
author = {Yuichi Futa and Yasunari Shidama},
title = {Dual Lattice of $\mathbb{Z}$-module Lattice},
journal = {Formalized Mathematics},
volume = {25},
year = {2017},
pages = {157-169},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0015}
}
Yuichi Futa; Yasunari Shidama. Dual Lattice of ℤ-module Lattice. Formalized Mathematics, Tome 25 (2017) pp. 157-169. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0015/