Properties of Primes and Multiplicative Group of a Field
Arai, Kenichi, Okazaki, Hiroyuki
Inferior Limit, Superior Limit and Convergence of Sequences of Extended Real Numbers
Yamazaki, Hiroshi, Endou, Noboru, Shidama, Yasunari, Okazaki, Hiroyuki
Matrix of ℤ-module1
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
N-Dimensional Binary Vector Spaces
Arai, Kenichi, Okazaki, Hiroyuki
Formalization of Orthogonal Decomposition for Hilbert Spaces
Okazaki, Hiroyuki
Banach’s Continuous Inverse Theorem and Closed Graph Theorem
Sakurai, Hideki, Okazaki, Hiroyuki, Shidama, Yasunari
Probability on Finite Set and Real-Valued Random Variables
Okazaki, Hiroyuki, Shidama, Yasunari
Z-modules
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
On the Formalization of Gram-Schmidt Process for Orthonormalizing a Set of Vectors
Okazaki, Hiroyuki
Difference of Function on Vector Space over F
Arai, Kenichi, Wakabayashi, Ken, Okazaki, Hiroyuki
Algebra of Polynomially Bounded Sequences and Negligible Functions
Okazaki, Hiroyuki
Formalization of Orthogonal Complements of Normed Spaces
Okazaki, Hiroyuki