http://hdl.handle.net/11320/3586 Mon, 01 Jun 2026 07:20:21 GMT 2026-06-01T07:20:21Z http://hdl.handle.net/11320/3659 Tytuł: On L1 Space Formed by Complex-Valued Partial Functions Autorzy: Watase, Yasushige; Endou, Noboru; Shidama, Yasunari Abstrakt: In this article, we formalized L1 space formed by complexvalued partial functions [11], [15]. The real-valued case was formalized in [22] and this article is its generalization. Sun, 01 Jan 2012 00:00:00 GMT http://hdl.handle.net/11320/3659 2012-01-01T00:00:00Z http://hdl.handle.net/11320/3658 Tytuł: Isomorphisms of Direct Products of Finite Cyclic Groups Autorzy: Arai, Kenichi; Okazaki, Hiroyuki; Shidama, Yasunari Abstrakt: In this article, we formalize that every finite cyclic group is isomorphic to a direct product of finite cyclic groups which orders are relative prime. This theorem is closely related to the Chinese Remainder theorem ([18]) and is a useful lemma to prove the basis theorem for finite abelian groups and the fundamental theorem of finite abelian groups. Moreover, we formalize some facts about the product of a finite sequence of abelian groups. Sun, 01 Jan 2012 00:00:00 GMT http://hdl.handle.net/11320/3658 2012-01-01T00:00:00Z http://hdl.handle.net/11320/3654 Tytuł: Cayley-Dickson Construction Autorzy: Korniłowicz, Artur Abstrakt: Cayley-Dickson construction produces a sequence of normed algebras over real numbers. Its consequent applications result in complex numbers, quaternions, octonions, etc. In this paper we formalize the construction and prove its basic properties. Sun, 01 Jan 2012 00:00:00 GMT http://hdl.handle.net/11320/3654 2012-01-01T00:00:00Z http://hdl.handle.net/11320/3653 Tytuł: Free Z-module Autorzy: Futa, Yuichi; Okazaki, Hiroyuki; Shidama, Yasunari Abstrakt: 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 Z-module. Sun, 01 Jan 2012 00:00:00 GMT http://hdl.handle.net/11320/3653 2012-01-01T00:00:00Z