Torsion part of \(\mathbb{Z}\)-module

DOI10.1515/FORMA-2015-0024zbMath1334.13008OpenAlexW2326370346MaRDI QIDQ271895

Yasunari Shidama, Hiroyuki Okazaki, Yuichi Futa

Publication date: 20 April 2016

Published in: Formalized Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1515/forma-2015-0024

zbMATH Keywords

torsion part of \(\mathbb{Z}\)-moduletorsion-free non free \(\mathbb{Z}\)-module

Mathematics Subject Classification ID

Projective and free modules and ideals in commutative rings (13C10) Mechanization of proofs and logical operations (03B35) Torsion modules and ideals in commutative rings (13C12)

Related Items (1)

Divisible \(\mathbb{Z}\)-modules

Uses Software

• Mizar

Cites Work

• Unnamed Item
• Unnamed Item
• Gaussian integers
• Submodule of free \(\mathbb Z\)-module
• Factoring polynomials with rational coefficients
• Rank of submodule, linear transformations and linearly independent subsets of \(\mathbb Z\)-module
• Torsion \(\mathbb Z\)-module and torsion-free \(\mathbb Z\)-module
• Quotient Module of Z-module
• Free ℤ-module
• Semantics of MML Query - Ordering
• Z-modules
• Mizar: State-of-the-art and Beyond

This page was built for publication: Torsion part of \(\mathbb{Z}\)-module