Formalization of Integral Linear Space
Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
Banach’s Continuous Inverse Theorem and Closed Graph Theorem
Hideki Sakurai, Hiroyuki Okazaki, Yasunari Shidama
Differentiable Functions into Real Normed Spaces
Hiroyuki Okazaki, Noboru Endou, Keiko Narita, Yasunari Shidama
More on Continuous Functions on Normed Linear Spaces
Hiroyuki Okazaki, Noboru Endou, Yasunari Shidama
Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm
Hiroyuki Okazaki, Koh-ichi Nagao, Yuichi Futa
The Ck Space
Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama
Extended Euclidean Algorithm and CRT Algorithm
Hiroyuki Okazaki, Yosiki Aoki, Yasunari Shidama
Matrix of ℤ-module1
Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
Cartesian Products of Family of Real Linear Spaces
Hiroyuki Okazaki, Noboru Endou, Yasunari Shidama
N-Dimensional Binary Vector Spaces
Kenichi Arai, Hiroyuki Okazaki
Constructing Binary Huffman Tree
Hiroyuki Okazaki, Yuichi Futa, Yasunari Shidama
Definition and Properties of Direct Sum Decomposition of Groups1
Kazuhisa Nakasho, Hiroshi Yamazaki, Hiroyuki Okazaki, Yasunari Shidama