Isomorphisms of Direct Products of Finite Commutative Groups
Okazaki, Hiroyuki, Yamazaki, Hiroshi, Shidama, Yasunari
Formalization of Orthogonal Decomposition for Hilbert Spaces
Okazaki, Hiroyuki
Probability Measure on Discrete Spaces and Algebra of Real-Valued Random Variables
Okazaki, Hiroyuki, Shidama, Yasunari
Hopf Extension Theorem of Measure
Endou, Noboru, Okazaki, Hiroyuki, Shidama, Yasunari
Random Variables and Product of Probability Spaces
Okazaki, Hiroyuki, Shidama, Yasunari
Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module
Nakasho, Kazuhisa, Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Formalization of Separable Version of Banach–Alaoglu Theorem
Okazaki, Hiroyuki, Mieno, Takehiko