Extended Euclidean Algorithm and CRT Algorithm
Okazaki, Hiroyuki, Aoki, Yosiki, Shidama, Yasunari
N-Dimensional Binary Vector Spaces
Arai, Kenichi, Okazaki, Hiroyuki
Cartesian Products of Family of Real Linear Spaces
Okazaki, Hiroyuki, Endou, Noboru, Shidama, Yasunari
Formalization of Orthogonal Decomposition for Hilbert Spaces
Okazaki, Hiroyuki
Algebra of Polynomially Bounded Sequences and Negligible Functions
Okazaki, Hiroyuki
Z-modules
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Binary Representation of Natural Numbers
Okazaki, Hiroyuki
Formalization of the Advanced Encryption Standard. Part I
Arai, Kenichi, Okazaki, Hiroyuki
Free ℤ-module
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Difference of Function on Vector Space over F
Arai, Kenichi, Wakabayashi, Ken, Okazaki, Hiroyuki
Equivalent Expressions of Direct Sum Decomposition of Groups1
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Yamazaki, Hiroshi, Shidama, Yasunari
Finite Dimensional Real Normed Spaces are Proper Metric Spaces
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Shidama, Yasunari