Double Sequences and Limits
Endou, Noboru, Okazaki, Hiroyuki, Shidama, Yasunari
Equivalent Expressions of Direct Sum Decomposition of Groups1
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Yamazaki, Hiroshi, Shidama, Yasunari
The 3-Fold Product Space of Real Normed Spaces and its Properties
Okazaki, Hiroyuki, Nakasho, Kazuhisa
Difference of Function on Vector Space over F
Arai, Kenichi, Wakabayashi, Ken, Okazaki, Hiroyuki
Formalization of the Advanced Encryption Standard. Part I
Arai, Kenichi, Okazaki, Hiroyuki
Free ℤ-module
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Polynomially Bounded Sequences and Polynomial Sequences
Okazaki, Hiroyuki, Futa, Yuichi
Properties of Primes and Multiplicative Group of a Field
Arai, Kenichi, Okazaki, Hiroyuki
Isomorphisms of Direct Products of Finite Commutative Groups
Okazaki, Hiroyuki, Yamazaki, Hiroshi, Shidama, Yasunari
Formalization of Separable Version of Banach–Alaoglu Theorem
Okazaki, Hiroyuki, Mieno, Takehiko
Banach Algebra of Bounded Complex-Valued Functionals
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
N-Dimensional Binary Vector Spaces
Arai, Kenichi, Okazaki, Hiroyuki