Divisible ℤ-modules

Yuichi Futa; Yasunari Shidama

Formalized Mathematics (2016)

  • Volume: 24, Issue: 1, page 37-47
  • ISSN: 1426-2630

Abstract

top
In this article, we formalize the definition of divisible ℤ-module and its properties in the Mizar system [3]. We formally prove that any non-trivial divisible ℤ-modules are not finitely-generated.We introduce a divisible ℤ-module, equivalent to a vector space of a torsion-free ℤ-module with a coefficient ring ℚ. ℤ-modules are important for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [15], cryptographic systems with lattices [16] and coding theory [8].

How to cite

top

Yuichi Futa, and Yasunari Shidama. "Divisible ℤ-modules." Formalized Mathematics 24.1 (2016): 37-47. <http://eudml.org/doc/286752>.

@article{YuichiFuta2016,
abstract = {In this article, we formalize the definition of divisible ℤ-module and its properties in the Mizar system [3]. We formally prove that any non-trivial divisible ℤ-modules are not finitely-generated.We introduce a divisible ℤ-module, equivalent to a vector space of a torsion-free ℤ-module with a coefficient ring ℚ. ℤ-modules are important for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [15], cryptographic systems with lattices [16] and coding theory [8].},
author = {Yuichi Futa, Yasunari Shidama},
journal = {Formalized Mathematics},
keywords = {divisible vector; divisible ℤ-module; divisible -module},
language = {eng},
number = {1},
pages = {37-47},
title = {Divisible ℤ-modules},
url = {http://eudml.org/doc/286752},
volume = {24},
year = {2016},
}

TY - JOUR
AU - Yuichi Futa
AU - Yasunari Shidama
TI - Divisible ℤ-modules
JO - Formalized Mathematics
PY - 2016
VL - 24
IS - 1
SP - 37
EP - 47
AB - In this article, we formalize the definition of divisible ℤ-module and its properties in the Mizar system [3]. We formally prove that any non-trivial divisible ℤ-modules are not finitely-generated.We introduce a divisible ℤ-module, equivalent to a vector space of a torsion-free ℤ-module with a coefficient ring ℚ. ℤ-modules are important for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [15], cryptographic systems with lattices [16] and coding theory [8].
LA - eng
KW - divisible vector; divisible ℤ-module; divisible -module
UR - http://eudml.org/doc/286752
ER -

References

top
  1. [1] Grzegorz Bancerek. Cardinal arithmetics. Formalized Mathematics, 1(3):543-547, 1990. 
  2. [2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  3. [3] 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. Zbl06512423
  4. [4] Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507-513, 1990. 
  5. [5] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55-65, 1990. 
  6. [6] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  7. [7] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  8. [8] Wolfgang Ebeling. Lattices and Codes. Advanced Lectures in Mathematics. Springer Fachmedien Wiesbaden, 2013. 
  9. [9] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. ℤ-modules. Formalized Mathematics, 20(1):47-59, 2012. doi:10.2478/v10037-012-0007-z. Zbl1276.94012
  10. [10] 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. Zbl06213839
  11. [11] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Free ℤ-module. Formalized Mathematics, 20(4):275-280, 2012. doi:10.2478/v10037-012-0033-x. Zbl06213848
  12. [12] Yuichi Futa, Hiroyuki Okazaki, Kazuhisa Nakasho, and Yasunari Shidama. Torsion ℤ-module and torsion-free Z-module. Formalized Mathematics, 22(4):277-289, 2014. doi:10.2478/forma-2014-0028. Zbl1316.13012
  13. [13] Yuichi Futa, Hiroyuki Okazaki, and Yasunari Shidama. Torsion part of ℤ-module. Formalized Mathematics, 23(4):297-307, 2015. doi:10.1515/forma-2015-0024. Zbl1334.13008
  14. [14] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990. 
  15. [15] A. K. Lenstra, H. W. Lenstra Jr., and L. Lovász. Factoring polynomials with rational coefficients. Mathematische Annalen, 261(4), 1982. 
  16. [16] Daniele Micciancio and Shafi Goldwasser. Complexity of lattice problems: A cryptographic perspective. The International Series in Engineering and Computer Science, 2002. Zbl1140.94010
  17. [17] Jan Popiołek. Some properties of functions modul and signum. Formalized Mathematics, 1(2):263-264, 1990. 
  18. [18] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990. 
  19. [19] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990. 
  20. [20] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73-83, 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.