Formalization of the Advanced Encryption Standard. Part I
Arai, Kenichi, Okazaki, Hiroyuki
Formalization of Separable Version of Banach–Alaoglu Theorem
Okazaki, Hiroyuki, Mieno, Takehiko
Finite Dimensional Real Normed Spaces are Proper Metric Spaces
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Shidama, Yasunari
Banach’s Continuous Inverse Theorem and Closed Graph Theorem
Sakurai, Hideki, Okazaki, Hiroyuki, Shidama, Yasunari
Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module
Nakasho, Kazuhisa, Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Gaussian Integers
Futa, Yuichi, Okazaki, Hiroyuki, Mizushima, Daichi, Shidama, Yasunari
N-Dimensional Binary Vector Spaces
Arai, Kenichi, Okazaki, Hiroyuki
Uniqueness of Factoring an Integer and Multiplicative Group Z/pZ*
Okazaki, Hiroyuki, Shidama, Yasunari
Isomorphisms of Direct Products of Finite Cyclic Groups
Arai, Kenichi, Okazaki, Hiroyuki, Shidama, Yasunari
Properties of Primes and Multiplicative Group of a Field
Arai, Kenichi, Okazaki, Hiroyuki
Formalization of Orthogonal Decomposition for Hilbert Spaces
Okazaki, Hiroyuki
Double Sequences and Limits
Endou, Noboru, Okazaki, Hiroyuki, Shidama, Yasunari