Finite Dimensional Real Normed Spaces are Proper Metric Spaces
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Shidama, Yasunari
Formalization of Orthogonal Decomposition for Hilbert Spaces
Okazaki, Hiroyuki
Isomorphisms of Direct Products of Finite Cyclic Groups
Arai, Kenichi, Okazaki, Hiroyuki, Shidama, Yasunari
Polynomially Bounded Sequences and Polynomial Sequences
Okazaki, Hiroyuki, Futa, Yuichi
Formalization of Integral Linear Space
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Double Sequences and Limits
Endou, Noboru, Okazaki, Hiroyuki, Shidama, Yasunari
Submodule of free Z-module
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Banach Algebra of Bounded Complex-Valued Functionals
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
On the Formalization of Gram-Schmidt Process for Orthonormalizing a Set of Vectors
Okazaki, Hiroyuki
Differentiable Functions into Real Normed Spaces
Okazaki, Hiroyuki, Endou, Noboru, Narita, Keiko, Shidama, Yasunari
Gaussian Integers
Futa, Yuichi, Okazaki, Hiroyuki, Mizushima, Daichi, Shidama, Yasunari
Uniqueness of Factoring an Integer and Multiplicative Group Z/pZ*
Okazaki, Hiroyuki, Shidama, Yasunari