http://hdl.handle.net/11320/4801 Mon, 01 Jun 2026 07:57:49 GMT 2026-06-01T07:57:49Z http://hdl.handle.net/11320/5492 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. Fri, 01 Jan 2016 00:00:00 GMT http://hdl.handle.net/11320/5492 2016-01-01T00:00:00Z http://hdl.handle.net/11320/5490 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]. Fri, 01 Jan 2016 00:00:00 GMT http://hdl.handle.net/11320/5490 2016-01-01T00:00:00Z http://hdl.handle.net/11320/5491 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. Fri, 01 Jan 2016 00:00:00 GMT http://hdl.handle.net/11320/5491 2016-01-01T00:00:00Z http://hdl.handle.net/11320/5489 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]. Fri, 01 Jan 2016 00:00:00 GMT http://hdl.handle.net/11320/5489 2016-01-01T00:00:00Z