Torsion Part of ℤ-module

Yuichi Futa; Hiroyuki Okazaki; Yasunari Shidama

doi:10.1515/forma-2015-0024

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

Torsion Part of ℤ-module

Formalized Mathematics

Volume 23 (2015): Issue 4 (December 2015)

By: Yuichi Futa, Hiroyuki Okazaki and Yasunari Shidama

Open Access

|Mar 2016

Abstract

In this article, we formalize in Mizar [7] the definition of “torsion part” of ℤ-module and its properties. We show ℤ-module generated by the field of rational numbers as an example of torsion-free non free ℤ-modules. We also formalize the rank-nullity theorem over finite-rank free ℤ-modules (previously formalized in [1]). ℤ-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [23] and cryptographic systems with lattices [24].

References

[1] Jesse Alama. The rank+nullity theorem. Formalized Mathematics, 15(3):137–142, 2007. doi:10.2478/v10037-007-0015-6.10.2478/v10037-007-0015-6
Search in Google Scholar
[2] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.
Search in Google Scholar
[3] Grzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543–547, 1990.
Search in Google Scholar
[4] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.
Search in Google Scholar
[5] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.
Search in Google Scholar
[6] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.
Search in Google Scholar
[7] 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
Search in Google Scholar
[8] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.
Search in Google Scholar
[9] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55–65, 1990.
Search in Google Scholar
[10] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.
Search in Google Scholar
[11] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990.
Search in Google Scholar
[12] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.
Search in Google Scholar
[13] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.
Search in Google Scholar
[14] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. ℤ-modules. Formalized Mathematics, 20(1):47–59, 2012. doi:10.2478/v10037-012-0007-z.10.2478/v10037-012-0007-z
Search in Google Scholar
[15] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Quotient module of ℤ-module. Formalized Mathematics, 20(3):205–214, 2012. doi:10.2478/v10037-012-0024-y.10.2478/v10037-012-0024-y
Search in Google Scholar
[16] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Free ℤ-module. Formalized Mathematics, 20(4):275–280, 2012. doi:10.2478/v10037-012-0033-x.10.2478/v10037-012-0033-x
Search in Google Scholar
[17] Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima, and Yasunari Shidama. Gaussian integers. Formalized Mathematics, 21(2):115–125, 2013. doi:10.2478/forma-2013-0013.10.2478/forma-2013-0013
Search in Google Scholar
[18] 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
Search in Google Scholar
[19] Yuichi Futa, Hiroyuki Okazaki, Kazuhisa Nakasho, and Yasunari Shidama. Torsion ℤ-module and torsion-free ℤ-module. Formalized Mathematics, 22(4):277–289, 2014. doi:10.2478/forma-2014-0028.10.2478/forma-2014-0028
Search in Google Scholar
[20] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841–845, 1990.
Search in Google Scholar
[21] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990.
Search in Google Scholar
[22] Rafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Formalized Mathematics, 1(5):829–832, 1990.
Search in Google Scholar
[23] A. K. Lenstra, H. W. Lenstra Jr., and L. Lovász. Factoring polynomials with rational coefficients. Mathematische Annalen, 261(4), 1982.10.1007/BF01457454
Search in Google Scholar
[24] 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
[25] Michał Muzalewski. Rings and modules – part II. Formalized Mathematics, 2(4):579–585, 1991.
Search in Google Scholar
[26] Kazuhisa Nakasho, Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Rank of submodule, linear transformations and linearly independent subsets of ℤ-module. Formalized Mathematics, 22(3):189–198, 2014. doi:10.2478/forma-2014-0021.10.2478/forma-2014-0021
Search in Google Scholar
[27] Christoph Schwarzweller. The binomial theorem for algebraic structures. Formalized Mathematics, 9(3):559–564, 2001.
Search in Google Scholar
[28] Christoph Schwarzweller. The ring of integers, Euclidean rings and modulo integers. Formalized Mathematics, 8(1):29–34, 1999.
Search in Google Scholar
[29] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1): 115–122, 1990.
Search in Google Scholar
[30] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990.
Search in Google Scholar
[31] Wojciech A. Trybulec. Operations on subspaces in real linear space. Formalized Mathematics, 1(2):395–399, 1990.
Search in Google Scholar
[32] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291–296, 1990.
Search in Google Scholar
[33] Wojciech A. Trybulec. Subspaces and cosets of subspaces in vector space. Formalized Mathematics, 1(5):865–870, 1990.
Search in Google Scholar
[34] Wojciech A. Trybulec. Operations on subspaces in vector space. Formalized Mathematics, 1(5):871–876, 1990.
Search in Google Scholar
[35] Wojciech A. Trybulec. Linear combinations in vector space. Formalized Mathematics, 1 (5):877–882, 1990.
Search in Google Scholar
[36] Wojciech A. Trybulec. Basis of vector space. Formalized Mathematics, 1(5):883–885, 1990.
Search in Google Scholar
[37] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.
Search in Google Scholar
[38] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73–83, 1990.
Search in Google Scholar
[39] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990.
Search in Google Scholar

Articles in this issue

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

Journal RSS Feed

Language: English

Page range: 297 - 307

Submitted on: Aug 14, 2015

Published on: Mar 25, 2016

Published by: University of Białystok

In partnership with: Paradigm Publishing Services

Publication frequency: 1 issue per year

Keywords:

15A03,

13C12,

03B35

Related subjects:

Mathematics,

Logic and set theory,

Computer sciences,

Artificial intelligence

© 2016 Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama, published by University of Białystok
This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Volume 23 (2015): Issue 4 (December 2015)