Real Vector Space and Related Notions
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Shidama, Yasunari
On the Formalization of Gram-Schmidt Process for Orthonormalizing a Set of Vectors
Okazaki, Hiroyuki
Isomorphisms of Direct Products of Cyclic Groups of Prime Power Order
Yamazaki, Hiroshi, Okazaki, Hiroyuki, Nakasho, Kazuhisa, Shidama, Yasunari
Formalization of the Advanced Encryption Standard. Part I
Arai, Kenichi, Okazaki, Hiroyuki
Formalization of Separable Version of Banach–Alaoglu Theorem
Okazaki, Hiroyuki, Mieno, Takehiko
Properties of Primes and Multiplicative Group of a Field
Arai, Kenichi, Okazaki, Hiroyuki
Polynomially Bounded Sequences and Polynomial Sequences
Okazaki, Hiroyuki, Futa, Yuichi