Displaying similar documents to “Torsion Z-module and Torsion-free Z-module”

Torsion Part of ℤ-module

Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama (2015)

Formalized Mathematics

Similarity:

In this article, we formalize in Mizar [7] the definition of “torsion part” of ℤ-module and its properties. We show ℤ-module generated by the field of rational numbers as an example of torsion-free non free ℤ-modules. We also formalize the rank-nullity theorem over finite-rank free ℤ-modules (previously formalized in [1]). ℤ-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [23] and cryptographic systems with lattices [24].

Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module

Kazuhisa Nakasho, Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama (2014)

Formalized Mathematics

Similarity:

In this article, we formalize some basic facts of Z-module. In the first section, we discuss the rank of submodule of Z-module and its properties. Especially, we formally prove that the rank of any Z-module is equal to or more than that of its submodules, and vice versa, and that there exists a submodule with any given rank that satisfies the above condition. In the next section, we mention basic facts of linear transformations between two Z-modules. In this section, we define homomorphism...

Free ℤ-module

Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama (2012)

Formalized Mathematics

Similarity:

In this article we formalize a free ℤ-module and its rank. We formally prove that for a free finite rank ℤ-module V , the number of elements in its basis, that is a rank of the ℤ-module, is constant regardless of the selection of its basis. ℤ-module is necessary for lattice problems, LLL(Lenstra, Lenstra and Lovász) base reduction algorithm and cryptographic systems with lattice [15]. Some theorems in this article are described by translating theorems in [21] and [8] into theorems of...

Divisible ℤ-modules

Yuichi Futa, Yasunari Shidama (2016)

Formalized Mathematics

Similarity:

In this article, we formalize the definition of divisible ℤ-module and its properties in the Mizar system [3]. We formally prove that any non-trivial divisible ℤ-modules are not finitely-generated.We introduce a divisible ℤ-module, equivalent to a vector space of a torsion-free ℤ-module with a coefficient ring ℚ. ℤ-modules are important for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [15], cryptographic systems with lattices [16] and coding theory [8]. ...

A functorial approach to the behaviour of multidimensional control systems

Jean-François Pommaret, Alban Quadrat (2003)

International Journal of Applied Mathematics and Computer Science

Similarity:

We show how to use the extension and torsion functors in order to compute the torsion submodule of a differential module associated with a multidimensional control system. In particular, we show that the concept of the weak primeness of matrices corresponds to the torsion-freeness of a certain module.