Torsion Part of ℤ-module

Yuichi Futa; Hiroyuki Okazaki; Yasunari Shidama

Formalized Mathematics (2015)

  • Volume: 23, Issue: 4, page 297-307
  • ISSN: 1426-2630

Abstract

top
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].

How to cite

top

Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. "Torsion Part of ℤ-module." Formalized Mathematics 23.4 (2015): 297-307. <http://eudml.org/doc/276870>.

@article{YuichiFuta2015,
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].},
author = {Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama},
journal = {Formalized Mathematics},
keywords = {torsion part of ℤ-module; torsion-free non free ℤ-module; torsion part of -module; torsion-free non free -module},
language = {eng},
number = {4},
pages = {297-307},
title = {Torsion Part of ℤ-module},
url = {http://eudml.org/doc/276870},
volume = {23},
year = {2015},
}

TY - JOUR
AU - Yuichi Futa
AU - Hiroyuki Okazaki
AU - Yasunari Shidama
TI - Torsion Part of ℤ-module
JO - Formalized Mathematics
PY - 2015
VL - 23
IS - 4
SP - 297
EP - 307
AB - 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].
LA - eng
KW - torsion part of ℤ-module; torsion-free non free ℤ-module; torsion part of -module; torsion-free non free -module
UR - http://eudml.org/doc/276870
ER -

References

top
  1. [1] Jesse Alama. The rank+nullity theorem. Formalized Mathematics, 15(3):137–142, 2007. doi:10.2478/v10037-007-0015-6.[Crossref] 
  2. [2] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990. 
  3. [3] Grzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543–547, 1990. 
  4. [4] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990. Zbl06213858
  5. [5] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990. 
  6. [6] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990. 
  7. [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.[Crossref] Zbl06512423
  8. [8] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990. 
  9. [9] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55–65, 1990. 
  10. [10] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990. 
  11. [11] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990. 
  12. [12] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990. 
  13. [13] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990. 
  14. [14] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. ℤ-modules. Formalized Mathematics, 20(1):47–59, 2012. doi:10.2478/v10037-012-0007-z.[Crossref] Zbl1276.94012
  15. [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.[Crossref] Zbl06213839
  16. [16] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Free ℤ-module. Formalized Mathematics, 20(4):275–280, 2012. doi:10.2478/v10037-012-0033-x.[Crossref] Zbl06213848
  17. [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.[Crossref] Zbl1298.11009
  18. [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.[Crossref] Zbl1298.13013
  19. [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.[Crossref] Zbl1316.13012
  20. [20] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5): 841–845, 1990. 
  21. [21] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335–342, 1990. 
  22. [22] Rafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relatively primes. Formalized Mathematics, 1(5):829–832, 1990. 
  23. [23] A. K. Lenstra, H. W. Lenstra Jr., and L. Lovász. Factoring polynomials with rational coefficients. Mathematische Annalen, 261(4), 1982. Zbl0477.68043
  24. [24] Daniele Micciancio and Shafi Goldwasser. Complexity of lattice problems: a cryptographic perspective. The International Series in Engineering and Computer Science, 2002. Zbl1140.94010
  25. [25] Michał Muzalewski. Rings and modules – part II. Formalized Mathematics, 2(4):579–585, 1991. 
  26. [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.[Crossref] Zbl1311.13009
  27. [27] Christoph Schwarzweller. The binomial theorem for algebraic structures. Formalized Mathematics, 9(3):559–564, 2001. 
  28. [28] Christoph Schwarzweller. The ring of integers, Euclidean rings and modulo integers. Formalized Mathematics, 8(1):29–34, 1999. 
  29. [29] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1): 115–122, 1990. 
  30. [30] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990. 
  31. [31] Wojciech A. Trybulec. Operations on subspaces in real linear space. Formalized Mathematics, 1(2):395–399, 1990. 
  32. [32] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291–296, 1990. 
  33. [33] Wojciech A. Trybulec. Subspaces and cosets of subspaces in vector space. Formalized Mathematics, 1(5):865–870, 1990. 
  34. [34] Wojciech A. Trybulec. Operations on subspaces in vector space. Formalized Mathematics, 1(5):871–876, 1990. 
  35. [35] Wojciech A. Trybulec. Linear combinations in vector space. Formalized Mathematics, 1 (5):877–882, 1990. 
  36. [36] Wojciech A. Trybulec. Basis of vector space. Formalized Mathematics, 1(5):883–885, 1990. 
  37. [37] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990. 
  38. [38] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73–83, 1990. 
  39. [39] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.