Uniqueness of Factoring an Integer and Multiplicative Group Z/pZ*
Okazaki, Hiroyuki, Shidama, Yasunari
Extended Euclidean Algorithm and CRT Algorithm
Okazaki, Hiroyuki, Aoki, Yosiki, Shidama, Yasunari
Cartesian Products of Family of Real Linear Spaces
Okazaki, Hiroyuki, Endou, Noboru, Shidama, Yasunari
Finite Dimensional Real Normed Spaces are Proper Metric Spaces
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Shidama, Yasunari
Inferior Limit, Superior Limit and Convergence of Sequences of Extended Real Numbers
Yamazaki, Hiroshi, Endou, Noboru, Shidama, Yasunari, Okazaki, Hiroyuki
Banach’s Continuous Inverse Theorem and Closed Graph Theorem
Sakurai, Hideki, Okazaki, Hiroyuki, Shidama, Yasunari
Random Variables and Product of Probability Spaces
Okazaki, Hiroyuki, Shidama, Yasunari
Formalization of Orthogonal Complements of Normed Spaces
Okazaki, Hiroyuki
Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module
Nakasho, Kazuhisa, Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Formalization of Separable Version of Banach–Alaoglu Theorem
Okazaki, Hiroyuki, Mieno, Takehiko
Constructing Binary Huffman Tree
Okazaki, Hiroyuki, Futa, Yuichi, Shidama, Yasunari
Formalization of the Data Encryption Standard
Okazaki, Hiroyuki, Shidama, Yasunari