<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

Published Online: Dec 31, 2014

Page range: 277 - 289

Received: Nov 29, 2014

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

Keywords
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

Published Online: Dec 31, 2014

Page range: 277 - 289

Received: Nov 29, 2014

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

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

Keywords
free Z-module, rank of Z-module, homomorphism of Z-module, linearly independent, linear combination