Formalization of Orthogonal Decomposition for Hilbert Spaces
Okazaki, Hiroyuki
Isomorphisms of Direct Products of Finite Commutative Groups
Okazaki, Hiroyuki, Yamazaki, Hiroshi, Shidama, Yasunari
Differentiable Functions into Real Normed Spaces
Okazaki, Hiroyuki, Endou, Noboru, Narita, Keiko, Shidama, Yasunari
Formalization of Integral Linear Space
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Functional Space C(ω), C0(ω)
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
Normal Subgroup of Product of Groups
Okazaki, Hiroyuki, Arai, Kenichi, Shidama, Yasunari
Equivalent Expressions of Direct Sum Decomposition of Groups1
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Yamazaki, Hiroshi, Shidama, Yasunari
Double Sequences and Limits
Endou, Noboru, Okazaki, Hiroyuki, Shidama, Yasunari
Formalization of the Advanced Encryption Standard. Part I
Arai, Kenichi, Okazaki, Hiroyuki
Free ℤ-module
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Hopf Extension Theorem of Measure
Endou, Noboru, Okazaki, Hiroyuki, Shidama, Yasunari
Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module
Nakasho, Kazuhisa, Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari