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

DOI10.1515/forma-2015-0024zbMath1334.13008MaRDI QIDQ271895

Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama

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}\)-module; torsion-free non free \(\mathbb{Z}\)-module

Mathematics Subject Classification ID

13C10: Projective and free modules and ideals in commutative rings

03B35: Mechanization of proofs and logical operations

13C12: Torsion modules and ideals in commutative rings

Uses Software

• Mizar