{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T05:38:04Z","timestamp":1648618684529},"reference-count":7,"publisher":"Walter de Gruyter GmbH","issue":"3","license":[{"start":{"date-parts":[[2017,10,1]],"date-time":"2017-10-01T00:00:00Z","timestamp":1506816000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,10,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p>In this article, we formalize in the Mizar system [1, 4] some properties of vector spaces over a ring. We formally prove the first isomorphism theorem of vector spaces over a ring. We also formalize the product space of vector spaces. \u2124-modules are useful for lattice problems such as LLL (Lenstra, Lenstra and Lov\u00e1sz) [5] base reduction algorithm and cryptographic systems [6, 2].<\/jats:p>","DOI":"10.1515\/forma-2017-0016","type":"journal-article","created":{"date-parts":[[2017,12,20]],"date-time":"2017-12-20T22:16:12Z","timestamp":1513808172000},"page":"171-178","source":"Crossref","is-referenced-by-count":0,"title":["Isomorphism Theorem on Vector Spaces over a Ring"],"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,12,19]]},"reference":[{"key":"2021040721433473118_j_forma-2017-0016_ref_001_w2aab3b7ab1b6b1ab1ab1Aa","unstructured":"[1] 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-8_17.10.1007\/978-3-319-20615-8_17"},{"key":"2021040721433473118_j_forma-2017-0016_ref_002_w2aab3b7ab1b6b1ab1ab2Aa","doi-asserted-by":"crossref","unstructured":"[2] Wolfgang Ebeling. Lattices and Codes. Advanced Lectures in Mathematics. Springer Fachmedien Wiesbaden, 2013.","DOI":"10.1007\/978-3-658-00360-9"},{"key":"2021040721433473118_j_forma-2017-0016_ref_003_w2aab3b7ab1b6b1ab1ab3Aa","unstructured":"[3] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Submodule of free \u2124-module. Formalized Mathematics, 21(4):273\u2013282, 2013. doi:10.2478\/forma-2013-0029.10.2478\/forma-2013-0029"},{"key":"2021040721433473118_j_forma-2017-0016_ref_004_w2aab3b7ab1b6b1ab1ab4Aa","unstructured":"[4] Adam Grabowski, Artur Korni\u0142owicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191\u2013198, 2015. doi:10.1007\/s10817-015-9345-1.10.1007\/s10817-015-9345-1"},{"key":"2021040721433473118_j_forma-2017-0016_ref_005_w2aab3b7ab1b6b1ab1ab5Aa","unstructured":"[5] 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":"2021040721433473118_j_forma-2017-0016_ref_006_w2aab3b7ab1b6b1ab1ab6Aa","doi-asserted-by":"crossref","unstructured":"[6] 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":"2021040721433473118_j_forma-2017-0016_ref_007_w2aab3b7ab1b6b1ab1ab7Aa","unstructured":"[7] Yasunari Shidama. Differentiable functions on normed linear spaces. Formalized Mathematics, 20(1):31\u201340, 2012. doi:10.2478\/v10037-012-0005-1.10.2478\/v10037-012-0005-1"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/25\/3\/article-p171.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2017-0016","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,8]],"date-time":"2021-04-08T03:54:23Z","timestamp":1617854063000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2017-0016"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,1]]},"references-count":7,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2017,12,19]]},"published-print":{"date-parts":[[2017,10,1]]}},"alternative-id":["10.1515\/forma-2017-0016"],"URL":"https:\/\/doi.org\/10.1515\/forma-2017-0016","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2017,10,1]]}}}