Finite Dimensional Real Normed Spaces are Proper Metric Spaces
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Shidama, Yasunari
Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm
Okazaki, Hiroyuki, Nagao, Koh-ichi, Futa, Yuichi
Formalization of Separable Version of Banach–Alaoglu Theorem
Okazaki, Hiroyuki, Mieno, Takehiko
Equivalent Expressions of Direct Sum Decomposition of Groups1
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Yamazaki, Hiroshi, Shidama, Yasunari
Formalization of the Data Encryption Standard
Okazaki, Hiroyuki, Shidama, Yasunari
Polynomially Bounded Sequences and Polynomial Sequences
Okazaki, Hiroyuki, Futa, Yuichi
Posterior Probability on Finite Set
Okazaki, Hiroyuki
Formalization of Orthogonal Complements of Normed Spaces
Okazaki, Hiroyuki
Extended Euclidean Algorithm and CRT Algorithm
Okazaki, Hiroyuki, Aoki, Yosiki, Shidama, Yasunari
Banach Algebra of Bounded Complex-Valued Functionals
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
Submodule of free Z-module
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
N-Dimensional Binary Vector Spaces
Arai, Kenichi, Okazaki, Hiroyuki