{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T11:43:10Z","timestamp":1648726990830},"reference-count":0,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2016,3,1]],"date-time":"2016-03-01T00:00:00Z","timestamp":1456790400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,3,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p> In this article, we formalize the definition of lattice of \u2124-module and its properties in the Mizar system [5].We formally prove that scalar products in lattices are bilinear forms over the field of real numbers \u211d. We also formalize the definitions of positive definite and integral lattices and their properties. Lattice of \u2124-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lov\u00e1sz) base reduction algorithm [14], and cryptographic systems with lattices [15] and coding theory [9].<\/jats:p>","DOI":"10.1515\/forma-2016-0005","type":"journal-article","created":{"date-parts":[[2016,8,22]],"date-time":"2016-08-22T14:36:23Z","timestamp":1471876583000},"page":"49-68","source":"Crossref","is-referenced-by-count":2,"title":["Lattice of \u2124-module"],"prefix":"10.1515","volume":"24","author":[{"given":"Yuichi","family":"Futa","sequence":"first","affiliation":[{"name":"Japan Advanced Institute of Science and Technology Ishikawa, 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":[[2016,8,31]]},"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/24\/1\/article-p49.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0005","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,6]],"date-time":"2021-04-06T22:13:20Z","timestamp":1617747200000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0005"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3,1]]},"references-count":0,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2016,8,31]]},"published-print":{"date-parts":[[2016,3,1]]}},"alternative-id":["10.1515\/forma-2016-0005"],"URL":"https:\/\/doi.org\/10.1515\/forma-2016-0005","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,3,1]]}}}