Torsion Z-module and Torsion-free Z-module

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

Full description

Bibliographic Details
Main Authors: Futa Yuichi, Okazaki Hiroyuki, Nakasho Kazuhisa, Shidama Yasunari
Format: Article
Language:English
Published: Sciendo 2014-12-01
Series:Formalized Mathematics
Subjects:
free z-module
rank of z-module
homomorphism of z-module
linearly independent
linear combination
Online Access:https://doi.org/10.2478/forma-2014-0028

Internet

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

Similar Items