<abstract xmlns="http://www.w3.org/1999/xhtml"><p> 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].</p></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].

Divisible ℤ-modules

Japan Advanced Institute of Science and Technology Ishikawa, Japan

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

{"article-title":"Divisible ℤ-modules"}

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

Divisible ℤ-modules

Online veröffentlicht: 31. Aug. 2016

Seitenbereich: 37 - 47

Eingereicht: 30. Dez. 2015

DOI: https://doi.org/10.1515/forma-2016-0004

Schlüsselwörter
divisible vector, divisible ℤ-module

© by Yuichi Futa

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Divisible ℤ-modules

Online veröffentlicht: 31. Aug. 2016

Seitenbereich: 37 - 47

Eingereicht: 30. Dez. 2015

DOI: https://doi.org/10.1515/forma-2016-0004

Schlüsselwörterdivisible vector, divisible ℤ-module

© by Yuichi Futa

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

Schlüsselwörter
divisible vector, divisible ℤ-module