Isomorphism Theorem on Vector Spaces over a Ring

Yuichi Futa; Yasunari Shidama

doi:10.1515/forma-2017-0016

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

Isomorphism Theorem on Vector Spaces over a Ring

Formalized Mathematics

Volume 25 (2017): Issue 3 (October 2017)

By: Yuichi Futa and Yasunari Shidama

Open Access

|Dec 2017

Abstract

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. ℤ-modules are useful for lattice problems such as LLL (Lenstra, Lenstra and Lovász) [5] base reduction algorithm and cryptographic systems [6, 2].

References

[1] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, 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–279. 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
Open DOI Search in Google Scholar Back to article
[2] Wolfgang Ebeling. Lattices and Codes. Advanced Lectures in Mathematics. Springer Fachmedien Wiesbaden, 2013.10.1007/978-3-658-00360-9
Search in Google Scholar Back to article
[3] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Submodule of free ℤ-module. Formalized Mathematics, 21(4):273–282, 2013. doi:10.2478/forma-2013-0029.10.2478/forma-2013-0029
Open DOI Search in Google Scholar Back to article
[4] 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
Open DOI Search in Google Scholar Back to article
[5] A. K. Lenstra, H. W. Lenstra Jr., and L. Lovász. Factoring polynomials with rational coefficients. Mathematische Annalen, 261(4):515–534, 1982. doi:10.1007/BF01457454.10.1007/BF01457454
Open DOI Search in Google Scholar Back to article
[6] 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
[7] Yasunari Shidama. Differentiable functions on normed linear spaces. Formalized Mathematics, 20(1):31–40, 2012. doi:10.2478/v10037-012-0005-1.10.2478/v10037-012-0005-1
Open DOI Search in Google Scholar Back to article

Articles in this issue

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

Journal RSS Feed

Language: English

Page range: 171 - 178

Submitted on: Aug 30, 2017

Published on: Dec 19, 2017

Published by: University of Białystok

In partnership with: Paradigm Publishing Services

Publication frequency: 1 issue per year

Keywords:

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-NonCommercial-NoDerivatives 3.0 License.

Volume 25 (2017): Issue 3 (October 2017)