Formalization of the Data Encryption Standard
Okazaki, Hiroyuki, Shidama, Yasunari
On Implicit and Inverse Function Theorems on Euclidean Spaces
Nakasho, Kazuhisa, Shidama, Yasunari
Functional Space C(ω), C0(ω)
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
Integral of Complex-Valued Measurable Function
Narita, Keiko, Endou, Noboru, Shidama, Yasunari
Egoroff's Theorem
Endou, Noboru, Shidama, Yasunari, Narita, Keiko
Isomorphisms of Direct Products of Finite Commutative Groups
Okazaki, Hiroyuki, Yamazaki, Hiroshi, Shidama, Yasunari
Uniform Boundedness Principle
Sakurai, Hideki, Kunimune, Hisayoshi, Shidama, Yasunari
Weak Convergence and Weak Convergence
Narita, Keiko, Shidama, Yasunari, Endou, Noboru
Higher Order Partial Differentiable Functions
Nakasho, Kazuhisa, Shidama, Yasunari
Submodule of free Z-module
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Bidual Spaces and Reflexivity of Real Normed Spaces
Narita, Keiko, Endou, Noboru, Shidama, Yasunari
Partial Differentiation of Vector-Valued Functions on n-Dimensional Real Normed Linear Spaces
Inoué, Takao, Naumowicz, Adam, Endou, Noboru, Shidama, Yasunari