Embedded Lattice and Properties of Gram Matrix

Yuichi Futa; Yasunari Shidama

doi:10.1515/forma-2017-0007

.blurhash-client-img { display: none !important; }

Embedded Lattice and Properties of Gram Matrix

Formalized Mathematics

Volume 25 (2017): Issue 1 (March 2017)

By: Yuichi Futa and Yasunari Shidama

Open Access

|May 2017

Abstract

In this article, we formalize in Mizar [14] the definition of embedding of lattice and its properties. We formally define an inner product on an embedded module. We also formalize properties of Gram matrix. We formally prove that an inverse of Gram matrix for a rational lattice exists. Lattice of Z-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lov´asz) base reduction algorithm [16] and cryptographic systems with lattice [17].

References

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.
Search in Google Scholar Back to article
[2] Grzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543-547, 1990.
Search in Google Scholar Back to article
[3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990.
Search in Google Scholar Back to article
[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.
Search in Google Scholar Back to article
[5] Czesław Bylinski. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529-536, 1990.
Search in Google Scholar Back to article
[6] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990.
Search in Google Scholar Back to article
[7] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
Search in Google Scholar Back to article
[8] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
Search in Google Scholar Back to article
[9] Yuichi Futa and Yasunari Shidama. Lattice of Z-module. Formalized Mathematics, 24 (1):49-68, 2016. doi: 10.1515/forma-2016-0005.10.1515/forma-2016-0005
Search in Google Scholar Back to article
[10] Yuichi Futa and Yasunari Shidama. Divisible Z-modules. Formalized Mathematics, 24 (1):37-47, 2016. doi: 10.1515/forma-2016-0004.10.1515/forma-2016-0004
Search in Google Scholar Back to article
[11] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Z-modules. Formalized Mathe matics, 20(1):47-59, 2012. doi: 10.2478/v10037-012-0007-z.10.2478/v10037-012-0007-z
Search in Google Scholar Back to article
[12] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Quotient module of Z-module. Formalized Mathematics, 20(3):205-214, 2012. doi: 10.2478/v10037-012-0024-y.10.2478/v10037-012-0024-y
Search in Google Scholar Back to article
[13] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Matrix of Z-module. Formalized Mathematics, 23(1):29-49, 2015. doi: 10.2478/forma-2015-0003.10.2478/forma-2015-0003
Search in Google Scholar Back to article
[14] Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191-198, 2015. doi: 10.1007/s10817-015-9345-1.10.1007/s10817-015-9345-1
Search in Google Scholar Back to article
[15] Eugeniusz Kusak, Wojciech Leonczuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990.
Search in Google Scholar Back to article
[16] A. K. Lenstra, H. W. Lenstra Jr., and L. Lov´asz. Factoring polynomials with rational coefficients. Mathematische Annalen, 261(4):515-534, 1982. doi: 10.1007/BF01457454.10.1007/BF01457454
Search in Google Scholar Back to article
[17] Daniele Micciancio and Shafi Goldwasser. Complexity of lattice problems: a cryptographic perspective. The International Series in Engineering and Computer Science, 2002.10.1007/978-1-4615-0897-7_8
Search in Google Scholar Back to article
[18] Michał Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3-11, 1991.
Search in Google Scholar Back to article
[19] Karol Pak. Basic properties of the rank of matrices over a field. Formalized Mathematics, 15(4):199-211, 2007. doi: 10.2478/v10037-007-0024-5.10.2478/v10037-007-0024-5
Search in Google Scholar Back to article
[20] Karol Pak and Andrzej Trybulec. Laplace expansion. Formalized Mathematics, 15(3): 143-150, 2007. doi: 10.2478/v10037-007-0016-5.10.2478/v10037-007-0016-5
Search in Google Scholar Back to article
[21] Nobuyuki Tamura and Yatsuka Nakamura. Determinant and inverse of matrices of real elements. Formalized Mathematics, 15(3):127-136, 2007. doi: 10.2478/v10037-007-0014-7.10.2478/v10037-007-0014-7
Search in Google Scholar Back to article
[22] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329-334, 1990.
Search in Google Scholar Back to article
[23] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569-573, 1990.
Search in Google Scholar Back to article
[24] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.
Search in Google Scholar Back to article
[25] Wojciech A. Trybulec. Subspaces and cosets of subspaces in vector space. Formalized Mathematics, 1(5):865-870, 1990.
Search in Google Scholar Back to article
[26] Wojciech A. Trybulec. Linear combinations in vector space. Formalized Mathematics, 1 (5):877-882, 1990.
Search in Google Scholar Back to article
[27] Wojciech A. Trybulec. Basis of vector space. Formalized Mathematics, 1(5):883-885, 1990.
Search in Google Scholar Back to article
[28] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
Search in Google Scholar Back to article
[29] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990.
Search in Google Scholar Back to article

Articles in this issue

DOI: https://doi.org/10.1515/forma-2017-0007 | Journal eISSN: 1898-9934 | Journal ISSN: 1426-2630

Journal RSS Feed

Language: English

Page range: 73 - 86

Submitted on: Mar 17, 2017

Published on: May 11, 2017

Published by: University of Białystok

In partnership with: Paradigm Publishing Services

Publication frequency: 1 issue per year

Keywords:

15A09,

15A63,

Related subjects:

Computer sciences, other

© 2017 Yuichi Futa, Yasunari Shidama, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Volume 25 (2017): Issue 1 (March 2017)