<abstract xmlns="http://www.w3.org/1999/xhtml"><p> In this article, we formalize a torsion Z-module and a torsionfree Z-module. Especially, we prove formally that finitely generated torsion-free Z-modules are finite rank free. We also formalize properties related to rank of finite rank free Z-modules. The notion of Z-module is necessary for solving lattice problems, LLL (Lenstra, Lenstra, and Lov´asz) base reduction algorithm [20], cryptographic systems with lattice [21], and coding theory [11].</p></abstract>

In this article, we formalize a torsion Z-module and a torsionfree Z-module. Especially, we prove formally that finitely generated torsion-free Z-modules are finite rank free. We also formalize properties related to rank of finite rank free Z-modules. The notion of Z-module is necessary for solving lattice problems, LLL (Lenstra, Lenstra, and Lov´asz) base reduction algorithm [20], cryptographic systems with lattice [21], and coding theory [11].

Torsion Z-module and Torsion-free Z-module

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":"Torsion Z-module and Torsion-free Z-module"}

In this article, we formalize a torsion Z-module and a torsionfree Z-module. Especially, we prove formally that finitely generated torsion-free Z-modules are...

Torsion Z-module and Torsion-free Z-module

Data publikacji: 31 gru 2014

Zakres stron: 277 - 289

Otrzymano: 29 lis 2014

DOI: https://doi.org/10.2478/forma-2014-0028

Słowa kluczowe
free Z-module, rank of Z-module, homomorphism of Z-module, linearly independent, linear combination

© by Yuichi Futa

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

Torsion Z-module and Torsion-free Z-module

Data publikacji: 31 gru 2014

Zakres stron: 277 - 289

Otrzymano: 29 lis 2014

DOI: https://doi.org/10.2478/forma-2014-0028

Słowa kluczowefree Z-module, rank of Z-module, homomorphism of Z-module, linearly independent, linear combination

© by Yuichi Futa

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

Słowa kluczowe
free Z-module, rank of Z-module, homomorphism of Z-module, linearly independent, linear combination