@MISC{GROUP_17.MIZ,
  AUTHOR = {Okazaki, Hiroyuki and Yamazaki, Hiroshi and Shidama, Yasunari},
  TITLE = {Isomorphisms of Direct Products of Finite Commutative Groups},
  NOTE = {The 1st author was supported by JSPS KAKENHI 21240001,
    and the 3rd author was supported by JSPS KAKENHI 22300285.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Direct Product of Finite Commutative Groups},
  SECTION3 = {Finite Direct Products of Finite Commutative Groups},
  DAY = {31},
  MONTH = {January},
  YEAR = {2013},
  ADDRESS1 = {Shinshu University, Nagano, JAPAN},
  ADDRESS2 = {Shinshu University, Nagano, JAPAN},
  ADDRESS3 = {Shinshu University, Nagano, JAPAN},
  SUMMARY = {We have been working on the formalization of groups.
  In \cite{GROUP_14.ABS}, we encoded some theorems concerning
  the product of cyclic groups. In this article, we present
  the generalized formalization of \cite{GROUP_14.ABS}.
  First, we show that every finite commutative group which
  order is composite number is isomorphic to a direct
  product of finite commutative groups which orders are relative prime.
  Next, we describe finite direct products of finite commutative groups.}}

