Gaussian Integers
Futa, Yuichi, Okazaki, Hiroyuki, Mizushima, Daichi, Shidama, Yasunari
Formalization of the Advanced Encryption Standard. Part I
Arai, Kenichi, Okazaki, Hiroyuki
Free ℤ-module
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
The Ck Space
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
Submodule of free Z-module
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Probability on Finite Set and Real-Valued Random Variables
Okazaki, Hiroyuki, Shidama, Yasunari
Functional Space C(ω), C0(ω)
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
Formalization of Orthogonal Decomposition for Hilbert Spaces
Okazaki, Hiroyuki
N-Dimensional Binary Vector Spaces
Arai, Kenichi, Okazaki, Hiroyuki
Banach Algebra of Bounded Complex-Valued Functionals
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
Polynomially Bounded Sequences and Polynomial Sequences
Okazaki, Hiroyuki, Futa, Yuichi
Real Vector Space and Related Notions
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Shidama, Yasunari