Formalization of Integral Linear Space
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Polynomially Bounded Sequences and Polynomial Sequences
Okazaki, Hiroyuki, Futa, Yuichi
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
Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module
Nakasho, Kazuhisa, Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Banach’s Continuous Inverse Theorem and Closed Graph Theorem
Sakurai, Hideki, Okazaki, Hiroyuki, Shidama, Yasunari