Operations of Points on Elliptic Curve in Projective Coordinates
Futa, Yuichi, Okazaki, Hiroyuki, Mizushima, Daichi, Shidama, Yasunari
The 3-Fold Product Space of Real Normed Spaces and its Properties
Okazaki, Hiroyuki, Nakasho, Kazuhisa
Isomorphisms of Direct Products of Cyclic Groups of Prime Power Order
Yamazaki, Hiroshi, Okazaki, Hiroyuki, Nakasho, Kazuhisa, Shidama, Yasunari
Cartesian Products of Family of Real Linear Spaces
Okazaki, Hiroyuki, Endou, Noboru, Shidama, Yasunari
Formalization of Separable Version of Banach–Alaoglu Theorem
Okazaki, Hiroyuki, Mieno, Takehiko
Formalization of the Advanced Encryption Standard. Part I
Arai, Kenichi, Okazaki, Hiroyuki
Probability Measure on Discrete Spaces and Algebra of Real-Valued Random Variables
Okazaki, Hiroyuki, Shidama, Yasunari
Functional Space C(ω), C0(ω)
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
Formalization of Orthogonal Complements of Normed Spaces
Okazaki, Hiroyuki
Probability on Finite Set and Real-Valued Random Variables
Okazaki, Hiroyuki, Shidama, Yasunari
Gaussian Integers
Futa, Yuichi, Okazaki, Hiroyuki, Mizushima, Daichi, Shidama, Yasunari
Inferior Limit, Superior Limit and Convergence of Sequences of Extended Real Numbers
Yamazaki, Hiroshi, Endou, Noboru, Shidama, Yasunari, Okazaki, Hiroyuki