Dual Lattice of ℤ-module Lattice

SummaryIn 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].Futa Yuichi - Tokyo University of Technology, Tokyo, JapanShidama Yasunari - Shinshu University, Nagano, JapanGrzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.Grzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543–547, 1990.Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi: 10.1007/978-3-319-20615-817.Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529–536, 1990.Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55–65, 1990.Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.Wolfgang Ebeling. Lattices and Codes. Advanced Lectures in Mathematics. Springer Fachmedien Wiesbaden, 2013.Yuichi Futa and Yasunari Shidama. Lattice of ℤ-module. Formalized Mathematics, 24 (1):49–68, 2016. doi: 10.1515/forma-2016-0005.Yuichi Futa and Yasunari Shidama. Embedded lattice and properties of Gram matrix. Formalized Mathematics, 25(1):73–86, 2017. doi: 10.1515/forma-2017-0007.Yuichi Futa and Yasunari Shidama. Divisible ℤ-modules. Formalized Mathematics, 24 (1):37–47, 2016. doi: 10.1515/forma-2016-0004.Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. ℤ-modules. Formalized Mathematics, 20(1):47–59, 2012. doi: 10.2478/v10037-012-0007-z.Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Quotient module of ℤ-module. Formalized Mathematics, 20(3):205–214, 2012. doi: 10.2478/v10037-012-0024-y.Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Matrix of ℤ-module. Formalized Mathematics, 23(1):29–49, 2015. doi: 10.2478/forma-2015-0003.Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841–845, 1990.Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.A. K. Lenstra, H. W. Lenstra Jr., and L. Lovász. Factoring polynomials with rational coefficients. Mathematische Annalen, 261(4):515–534, 1982. doi: 10.1007/BF01457454.Daniele Micciancio and Shafi Goldwasser. Complexity of lattice problems: a cryptographic perspective. The International Series in Engineering and Computer Science, 2002.Andrzej Trybulec. Function domains and Frænkel operator. Formalized Mathematics, 1 (3):495–500, 1990.Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569–573, 1990.Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575–579, 1990.Wojciech A. Trybulec. Linear combinations in vector space. Formalized Mathematics, 1 (5):877–882, 1990.Wojciech A. Trybulec. Basis of vector space. Formalized Mathematics, 1(5):883–885, 1990.Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73–83, 1990.25215716