{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T16:03:03Z","timestamp":1649088183099},"reference-count":29,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2017,3,28]],"date-time":"2017-03-28T00:00:00Z","timestamp":1490659200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/3.0\/legalcode"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,3,28]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p> 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\u00b4asz) base reduction algorithm [16] and cryptographic systems with lattice [17].<\/jats:p>","DOI":"10.1515\/forma-2017-0007","type":"journal-article","created":{"date-parts":[[2017,5,19]],"date-time":"2017-05-19T10:01:47Z","timestamp":1495188107000},"page":"73-86","source":"Crossref","is-referenced-by-count":1,"title":["Embedded Lattice and Properties of Gram Matrix"],"prefix":"10.1515","volume":"25","author":[{"given":"Yuichi","family":"Futa","sequence":"first","affiliation":[{"name":"Tokyo University of Technology , Tokyo , Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yasunari","family":"Shidama","sequence":"additional","affiliation":[{"name":"Shinshu University , Nagano , Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2017,5,11]]},"reference":[{"key":"2021040813183439326_j_forma-2017-0007_ref_001_w2aab2b8b2b1b7b1ab1ab1Aa","unstructured":"[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_002_w2aab2b8b2b1b7b1ab1ab2Aa","unstructured":"[2] Grzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543-547, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_003_w2aab2b8b2b1b7b1ab1ab3Aa","unstructured":"[3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_004_w2aab2b8b2b1b7b1ab1ab4Aa","unstructured":"[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_005_w2aab2b8b2b1b7b1ab1ab5Aa","unstructured":"[5] Czes\u0142aw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529-536, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_006_w2aab2b8b2b1b7b1ab1ab6Aa","unstructured":"[6] Czes\u0142aw Byli\u0144ski. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_007_w2aab2b8b2b1b7b1ab1ab7Aa","unstructured":"[7] Czes\u0142aw Byli\u0144ski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_008_w2aab2b8b2b1b7b1ab1ab8Aa","unstructured":"[8] Czes\u0142aw Byli\u0144ski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_009_w2aab2b8b2b1b7b1ab1ab9Aa","doi-asserted-by":"crossref","unstructured":"[9] Yuichi Futa and Yasunari Shidama. Lattice of Z-module. Formalized Mathematics, 24 (1):49-68, 2016. doi: 10.1515\/forma-2016-0005.","DOI":"10.1515\/forma-2016-0005"},{"key":"2021040813183439326_j_forma-2017-0007_ref_010_w2aab2b8b2b1b7b1ab1ac10Aa","doi-asserted-by":"crossref","unstructured":"[10] Yuichi Futa and Yasunari Shidama. Divisible Z-modules. Formalized Mathematics, 24 (1):37-47, 2016. doi: 10.1515\/forma-2016-0004.","DOI":"10.1515\/forma-2016-0004"},{"key":"2021040813183439326_j_forma-2017-0007_ref_011_w2aab2b8b2b1b7b1ab1ac11Aa","doi-asserted-by":"crossref","unstructured":"[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.","DOI":"10.2478\/v10037-012-0007-z"},{"key":"2021040813183439326_j_forma-2017-0007_ref_012_w2aab2b8b2b1b7b1ab1ac12Aa","doi-asserted-by":"crossref","unstructured":"[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.","DOI":"10.2478\/v10037-012-0024-y"},{"key":"2021040813183439326_j_forma-2017-0007_ref_013_w2aab2b8b2b1b7b1ab1ac13Aa","doi-asserted-by":"crossref","unstructured":"[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.","DOI":"10.2478\/forma-2015-0003"},{"key":"2021040813183439326_j_forma-2017-0007_ref_014_w2aab2b8b2b1b7b1ab1ac14Aa","doi-asserted-by":"crossref","unstructured":"[14] Adam Grabowski, Artur Korni\u0142owicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191-198, 2015. doi: 10.1007\/s10817-015-9345-1.","DOI":"10.1007\/s10817-015-9345-1"},{"key":"2021040813183439326_j_forma-2017-0007_ref_015_w2aab2b8b2b1b7b1ab1ac15Aa","unstructured":"[15] Eugeniusz Kusak, Wojciech Leonczuk, and Micha\u0142 Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_016_w2aab2b8b2b1b7b1ab1ac16Aa","doi-asserted-by":"crossref","unstructured":"[16] A. K. Lenstra, H. W. Lenstra Jr., and L. Lov\u00b4asz. Factoring polynomials with rational coefficients. Mathematische Annalen, 261(4):515-534, 1982. doi: 10.1007\/BF01457454.","DOI":"10.1007\/BF01457454"},{"key":"2021040813183439326_j_forma-2017-0007_ref_017_w2aab2b8b2b1b7b1ab1ac17Aa","doi-asserted-by":"crossref","unstructured":"[17] Daniele Micciancio and Shafi Goldwasser. Complexity of lattice problems: a cryptographic perspective. The International Series in Engineering and Computer Science, 2002.","DOI":"10.1007\/978-1-4615-0897-7_8"},{"key":"2021040813183439326_j_forma-2017-0007_ref_018_w2aab2b8b2b1b7b1ab1ac18Aa","unstructured":"[18] Micha\u0142 Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Formalized Mathematics, 2(1):3-11, 1991."},{"key":"2021040813183439326_j_forma-2017-0007_ref_019_w2aab2b8b2b1b7b1ab1ac19Aa","doi-asserted-by":"crossref","unstructured":"[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.","DOI":"10.2478\/v10037-007-0024-5"},{"key":"2021040813183439326_j_forma-2017-0007_ref_020_w2aab2b8b2b1b7b1ab1ac20Aa","doi-asserted-by":"crossref","unstructured":"[20] Karol Pak and Andrzej Trybulec. Laplace expansion. Formalized Mathematics, 15(3): 143-150, 2007. doi: 10.2478\/v10037-007-0016-5.","DOI":"10.2478\/v10037-007-0016-5"},{"key":"2021040813183439326_j_forma-2017-0007_ref_021_w2aab2b8b2b1b7b1ab1ac21Aa","doi-asserted-by":"crossref","unstructured":"[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.","DOI":"10.2478\/v10037-007-0014-7"},{"key":"2021040813183439326_j_forma-2017-0007_ref_022_w2aab2b8b2b1b7b1ab1ac22Aa","unstructured":"[22] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329-334, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_023_w2aab2b8b2b1b7b1ab1ac23Aa","unstructured":"[23] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569-573, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_024_w2aab2b8b2b1b7b1ab1ac24Aa","unstructured":"[24] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_025_w2aab2b8b2b1b7b1ab1ac25Aa","unstructured":"[25] Wojciech A. Trybulec. Subspaces and cosets of subspaces in vector space. Formalized Mathematics, 1(5):865-870, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_026_w2aab2b8b2b1b7b1ab1ac26Aa","unstructured":"[26] Wojciech A. Trybulec. Linear combinations in vector space. Formalized Mathematics, 1 (5):877-882, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_027_w2aab2b8b2b1b7b1ab1ac27Aa","unstructured":"[27] Wojciech A. Trybulec. Basis of vector space. Formalized Mathematics, 1(5):883-885, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_028_w2aab2b8b2b1b7b1ab1ac28Aa","unstructured":"[28] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990."},{"key":"2021040813183439326_j_forma-2017-0007_ref_029_w2aab2b8b2b1b7b1ab1ac29Aa","unstructured":"[29] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 1990."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/25\/1\/article-p73.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2017-0007","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,9]],"date-time":"2021-04-09T16:00:14Z","timestamp":1617984014000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2017-0007"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,28]]},"references-count":29,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2017,5,11]]},"published-print":{"date-parts":[[2017,3,28]]}},"alternative-id":["10.1515\/forma-2017-0007"],"URL":"https:\/\/doi.org\/10.1515\/forma-2017-0007","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,3,28]]}}}