http://hdl.handle.net/11320/3586 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. 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. 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. 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. 2012-01-01T00:00:00Z