{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T21:03:09Z","timestamp":1649019789795},"reference-count":27,"publisher":"Walter de Gruyter GmbH","issue":"2","license":[{"start":{"date-parts":[[2017,7,1]],"date-time":"2017-07-01T00:00:00Z","timestamp":1498867200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,7,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p>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 \u2124-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lov\u00e1sz) base reduction algorithm and cryptographic systems with lattice [20], [10] and [19].<\/jats:p>","DOI":"10.1515\/forma-2017-0015","type":"journal-article","created":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T10:00:55Z","timestamp":1506333655000},"page":"157-169","source":"Crossref","is-referenced-by-count":0,"title":["Dual Lattice of \u2124-module Lattice"],"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,9,23]]},"reference":[{"key":"2021040701563104242_j_forma-2017-0015_ref_001_w2aab3b7b7b1b6b1ab1ab1Aa","unstructured":"[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377\u2013382, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_002_w2aab3b7b7b1b6b1ab1ab2Aa","unstructured":"[2] Grzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543\u2013547, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_003_w2aab3b7b7b1b6b1ab1ab3Aa","unstructured":"[3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41\u201346, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_004_w2aab3b7b7b1b6b1ab1ab4Aa","unstructured":"[4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107\u2013114, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_005_w2aab3b7b7b1b6b1ab1ab5Aa","unstructured":"[5] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol P\u0105k, 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\u2013279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi: 10.1007\/978-3-319-20615-817.10.1007\/978-3-319-20615-817"},{"key":"2021040701563104242_j_forma-2017-0015_ref_006_w2aab3b7b7b1b6b1ab1ab6Aa","unstructured":"[6] Czes\u0142aw Byli\u0144ski. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529\u2013536, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_007_w2aab3b7b7b1b6b1ab1ab7Aa","unstructured":"[7] Czes\u0142aw Byli\u0144ski. Functions and their basic properties. Formalized Mathematics, 1(1): 55\u201365, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_008_w2aab3b7b7b1b6b1ab1ab8Aa","unstructured":"[8] Czes\u0142aw Byli\u0144ski. Functions from a set to a set. Formalized Mathematics, 1(1):153\u2013164, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_009_w2aab3b7b7b1b6b1ab1ab9Aa","unstructured":"[9] Czes\u0142aw Byli\u0144ski. Some basic properties of sets. Formalized Mathematics, 1(1):47\u201353, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_010_w2aab3b7b7b1b6b1ab1ac10Aa","doi-asserted-by":"crossref","unstructured":"[10] Wolfgang Ebeling. Lattices and Codes. Advanced Lectures in Mathematics. Springer Fachmedien Wiesbaden, 2013.","DOI":"10.1007\/978-3-658-00360-9"},{"key":"2021040701563104242_j_forma-2017-0015_ref_011_w2aab3b7b7b1b6b1ab1ac11Aa","unstructured":"[11] Yuichi Futa and Yasunari Shidama. Lattice of \u2124-module. Formalized Mathematics, 24 (1):49\u201368, 2016. doi: 10.1515\/forma-2016-0005.10.1515\/forma-2016-0005"},{"key":"2021040701563104242_j_forma-2017-0015_ref_012_w2aab3b7b7b1b6b1ab1ac12Aa","unstructured":"[12] Yuichi Futa and Yasunari Shidama. Embedded lattice and properties of Gram matrix. Formalized Mathematics, 25(1):73\u201386, 2017. doi: 10.1515\/forma-2017-0007.10.1515\/forma-2017-0007"},{"key":"2021040701563104242_j_forma-2017-0015_ref_013_w2aab3b7b7b1b6b1ab1ac13Aa","unstructured":"[13] Yuichi Futa and Yasunari Shidama. Divisible \u2124-modules. Formalized Mathematics, 24 (1):37\u201347, 2016. doi: 10.1515\/forma-2016-0004.10.1515\/forma-2016-0004"},{"key":"2021040701563104242_j_forma-2017-0015_ref_014_w2aab3b7b7b1b6b1ab1ac14Aa","unstructured":"[14] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. \u2124-modules. Formalized Mathematics, 20(1):47\u201359, 2012. doi: 10.2478\/v10037-012-0007-z.10.2478\/v10037-012-0007-z"},{"key":"2021040701563104242_j_forma-2017-0015_ref_015_w2aab3b7b7b1b6b1ab1ac15Aa","unstructured":"[15] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Quotient module of \u2124-module. Formalized Mathematics, 20(3):205\u2013214, 2012. doi: 10.2478\/v10037-012-0024-y.10.2478\/v10037-012-0024-y"},{"key":"2021040701563104242_j_forma-2017-0015_ref_016_w2aab3b7b7b1b6b1ab1ac16Aa","unstructured":"[16] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Matrix of \u2124-module. Formalized Mathematics, 23(1):29\u201349, 2015. doi: 10.2478\/forma-2015-0003.10.2478\/forma-2015-0003"},{"key":"2021040701563104242_j_forma-2017-0015_ref_017_w2aab3b7b7b1b6b1ab1ac17Aa","unstructured":"[17] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841\u2013845, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_018_w2aab3b7b7b1b6b1ab1ac18Aa","unstructured":"[18] Eugeniusz Kusak, Wojciech Leo\u0144czuk, and Micha\u0142 Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335\u2013342, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_019_w2aab3b7b7b1b6b1ab1ac19Aa","unstructured":"[19] A. K. Lenstra, H. W. Lenstra Jr., and L. Lov\u00e1sz. Factoring polynomials with rational coefficients. Mathematische Annalen, 261(4):515\u2013534, 1982. doi: 10.1007\/BF01457454.10.1007\/BF01457454"},{"key":"2021040701563104242_j_forma-2017-0015_ref_020_w2aab3b7b7b1b6b1ab1ac20Aa","doi-asserted-by":"crossref","unstructured":"[20] 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":"2021040701563104242_j_forma-2017-0015_ref_021_w2aab3b7b7b1b6b1ab1ac21Aa","unstructured":"[21] Andrzej Trybulec. Function domains and Fr\u00e6nkel operator. Formalized Mathematics, 1 (3):495\u2013500, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_022_w2aab3b7b7b1b6b1ab1ac22Aa","unstructured":"[22] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569\u2013573, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_023_w2aab3b7b7b1b6b1ab1ac23Aa","unstructured":"[23] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575\u2013579, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_024_w2aab3b7b7b1b6b1ab1ac24Aa","unstructured":"[24] Wojciech A. Trybulec. Linear combinations in vector space. Formalized Mathematics, 1 (5):877\u2013882, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_025_w2aab3b7b7b1b6b1ab1ac25Aa","unstructured":"[25] Wojciech A. Trybulec. Basis of vector space. Formalized Mathematics, 1(5):883\u2013885, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_026_w2aab3b7b7b1b6b1ab1ac26Aa","unstructured":"[26] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67\u201371, 1990."},{"key":"2021040701563104242_j_forma-2017-0015_ref_027_w2aab3b7b7b1b6b1ab1ac27Aa","unstructured":"[27] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73\u201383, 1990."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/25\/2\/article-p157.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2017-0015","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,7]],"date-time":"2021-04-07T05:18:29Z","timestamp":1617772709000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2017-0015"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,1]]},"references-count":27,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2017,9,23]]},"published-print":{"date-parts":[[2017,7,1]]}},"alternative-id":["10.1515\/forma-2017-0015"],"URL":"https:\/\/doi.org\/10.1515\/forma-2017-0015","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2017,7,1]]}}}