Banach’s Continuous Inverse Theorem and Closed Graph Theorem
Sakurai, Hideki, Okazaki, Hiroyuki, Shidama, Yasunari
Conservation Rules of Direct Sum Decomposition of Groups
Nakasho, Kazuhisa, Yamazaki, Hiroshi, Okazaki, Hiroyuki, Shidama, Yasunari
Z-modules
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Isomorphisms of Direct Products of Finite Cyclic Groups
Arai, Kenichi, Okazaki, Hiroyuki, Shidama, Yasunari
N-Dimensional Binary Vector Spaces
Arai, Kenichi, Okazaki, Hiroyuki
Torsion Z-module and Torsion-free Z-module
Futa, Yuichi, Okazaki, Hiroyuki, Nakasho, Kazuhisa, Shidama, Yasunari
Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module
Nakasho, Kazuhisa, Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Formalization of Orthogonal Decomposition for Hilbert Spaces
Okazaki, Hiroyuki
Equivalent Expressions of Direct Sum Decomposition of Groups1
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Yamazaki, Hiroshi, Shidama, Yasunari
Banach Algebra of Bounded Complex-Valued Functionals
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
Properties of Primes and Multiplicative Group of a Field
Arai, Kenichi, Okazaki, Hiroyuki
Formalization of the Advanced Encryption Standard. Part I
Arai, Kenichi, Okazaki, Hiroyuki