Operations of Points on Elliptic Curve in Affine Coordinates
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Real Vector Space and Related Notions
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Shidama, Yasunari
The Ck Space
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
Isomorphisms of Direct Products of Cyclic Groups of Prime Power Order
Yamazaki, Hiroshi, Okazaki, Hiroyuki, Nakasho, Kazuhisa, Shidama, Yasunari
Formalization of the Advanced Encryption Standard. Part I
Arai, Kenichi, Okazaki, Hiroyuki
Z-modules
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Conservation Rules of Direct Sum Decomposition of Groups
Nakasho, Kazuhisa, Yamazaki, Hiroshi, Okazaki, Hiroyuki, Shidama, Yasunari
The 3-Fold Product Space of Real Normed Spaces and its Properties
Okazaki, Hiroyuki, Nakasho, Kazuhisa
Formalization of Separable Version of Banach–Alaoglu Theorem
Okazaki, Hiroyuki, Mieno, Takehiko
Polynomially Bounded Sequences and Polynomial Sequences
Okazaki, Hiroyuki, Futa, Yuichi
Probability Measure on Discrete Spaces and Algebra of Real-Valued Random Variables
Okazaki, Hiroyuki, Shidama, Yasunari
Finite Dimensional Real Normed Spaces are Proper Metric Spaces
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Shidama, Yasunari