Formalization of Orthogonal Decomposition for Hilbert Spaces
Okazaki, Hiroyuki
Formalization of Orthogonal Complements of Normed Spaces
Okazaki, Hiroyuki
Z-modules
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Probability on Finite and Discrete Set and Uniform Distribution
Okazaki, Hiroyuki
Torsion Part of ℤ-module
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Isomorphisms of Direct Products of Finite Commutative Groups
Okazaki, Hiroyuki, Yamazaki, Hiroshi, Shidama, Yasunari
Functional Space C(ω), C0(ω)
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module
Nakasho, Kazuhisa, Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Normal Subgroup of Product of Groups
Okazaki, Hiroyuki, Arai, Kenichi, Shidama, Yasunari
On the Formalization of Gram-Schmidt Process for Orthonormalizing a Set of Vectors
Okazaki, Hiroyuki
Algebra of Polynomially Bounded Sequences and Negligible Functions
Okazaki, Hiroyuki
Submodule of free Z-module
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari