http://hdl.handle.net/11320/4801 2026-06-01T07:57:49Z 2026-06-01T07:57:49Z Nakasho, Kazuhisa Yamazaki, Hiroshi Okazaki, Hiroyuki Shidama, Yasunari http://hdl.handle.net/11320/5492 2017-10-05T23:13:34Z 2016-01-01T00:00:00Z

Tytuł: Conservation Rules of Direct Sum Decomposition of Groups Autorzy: Nakasho, Kazuhisa; Yamazaki, Hiroshi; Okazaki, Hiroyuki; Shidama, Yasunari Abstrakt: In this article, conservation rules of the direct sum decomposition of groups are mainly discussed. In the first section, we prepare miscellaneous definitions and theorems for further formalization in Mizar [5]. In the next three sections, we formalized the fact that the property of direct sum decomposition is preserved against the substitutions of the subscript set, flattening of direct sum, and layering of direct sum, respectively. We referred to [14], [13] [6] and [11] in the formalization.

2016-01-01T00:00:00Z Futa, Yuichi Shidama, Yasunari http://hdl.handle.net/11320/5490 2017-10-05T23:13:31Z 2016-01-01T00:00:00Z

Tytuł: Lattice of ℤ-module Autorzy: Futa, Yuichi; Shidama, Yasunari Abstrakt: In this article, we formalize the definition of lattice of ℤ-module and its properties in the Mizar system [5].We formally prove that scalar products in lattices are bilinear forms over the field of real numbers ℝ. We also formalize the definitions of positive definite and integral lattices and their properties. Lattice of ℤ-module is necessary for lattice problems, LLL (Lenstra, Lenstra and Lovász) base reduction algorithm [14], and cryptographic systems with lattices [15] and coding theory [9].

2016-01-01T00:00:00Z Endou, Noboru http://hdl.handle.net/11320/5491 2017-10-05T23:13:32Z 2016-01-01T00:00:00Z

Tytuł: Product Pre-Measure Autorzy: Endou, Noboru Abstrakt: In this article we formalize in Mizar [5] product pre-measure on product sets of measurable sets. Although there are some approaches to construct product measure [22], [6], [9], [21], [25], we start it from σ-measure because existence of σ-measure on any semialgebras has been proved in [15]. In this approach, we use some theorems for integrals.

2016-01-01T00:00:00Z Futa, Yuichi Shidama, Yasunari http://hdl.handle.net/11320/5489 2017-10-05T23:13:30Z 2016-01-01T00:00:00Z

Tytuł: Divisible ℤ-modules Autorzy: Futa, Yuichi; Shidama, Yasunari Abstrakt: 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].

2016-01-01T00:00:00Z