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

DOI10.1515/forma-2016-0004zbMath1343.13014OpenAlexW2508409595MaRDI QIDQ306629

Yasunari Shidama, Yuichi Futa

Publication date: 1 September 2016

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

Full work available at URL: https://doi.org/10.1515/forma-2016-0004

zbMATH Keywords

divisible \(\mathbb{Z}\)-moduledivisible vector

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure, classification theorems for modules and ideals in commutative rings (13C05) Vector spaces, linear dependence, rank, lineability (15A03) Other special types of modules and ideals in commutative rings (13C13)

Related Items

Dual lattice of \(\mathbb{Z}\)-module lattice ⋮ Embedded lattice and properties of Gram matrix

Uses Software

• Mizar

Cites Work

• Torsion part of \(\mathbb{Z}\)-module
• Factoring polynomials with rational coefficients
• Torsion \(\mathbb Z\)-module and torsion-free \(\mathbb Z\)-module
• Quotient Module of Z-module
• Free ℤ-module
• Semantics of MML Query - Ordering
• Z-modules
• Lattices and Codes
• Mizar: State-of-the-art and Beyond
• Unnamed Item