@MISC{GROUP_20.MIZ,
  AUTHOR = {Nakasho, Kazuhisa and Okazaki, Hiroyuki and
    Yamazaki, Hiroshi and Shidama, Yasunari},
  TITLE = {Equivalent Expressions of Direct Sum Decomposition of Groups},
  SECTION1 = {Internal Direct Sum Decomposition into Normal Subgroups},
  SECTION2 = {Internal Direct Sum Decomposition for Commutative Group},
  SECTION3 = {Equivalence between Internal and External Direct Sum},
  DAY = {26},
  MONTH = {February},
  YEAR = {2015},
  ADDRESS2 = {Shinshu University, Nagano, Japan},
  ADDRESS2 = {Shinshu University, Nagano, Japan},
  ADDRESS3 = {Shinshu University, Nagano, Japan},
  ADDRESS4 = {Shinshu University, Nagano, Japan},
  SUMMARY = {In this article, the equivalent expressions of the direct sum
   decomposition of groups are mainly discussed.
   In the first section, we formalize the fact that the internal direct sum
   decomposition can be defined as normal subgroups and some of their properties.
   In the second section, we formalize an equivalent form of internal direct sum
   of of commutative groups.
   In the last section, we formalize that the external direct sum leads
   an internal direct sum.
   We referred to \cite{rotman1995introduction}, \cite{robinson2012course}
   \cite{BourbakiAlgI} and \cite{lang-algebra} in the formalization.},
  ACKNOWLEDGEMENT = {This work was supported by JSPS KAKENHI 22300285.}}

@book{rotman1995introduction,
  AUTHOR    = {Rotman, J.J.},
  TITLE     = {An Introduction to the Theory of Groups},
  PUBLISHER = {Springer},
  YEAR      = {1995}
}

@book{robinson2012course,
  AUTHOR    = {Robinson, D.},
  TITLE     = {A Course in the Theory of Groups},
  PUBLISHER = {Springer New York},
  YEAR      = {2012}
}

@BOOK{BourbakiAlgI,
  AUTHOR    = {Bourbaki, Nicolas},
  TITLE     = {Elements of Mathematics. {A}lgebra {I}. {C}hapters 1--3},
  PUBLISHER = {Springer-Verlag},
  YEAR      = {1989},
  ADDRESS   = {Berlin, Heidelberg, New York, London, Paris, Tokyo}}

@BOOK{lang-algebra,
  AUTHOR    = {Lang, Serge},
  TITLE     = {Algebra},
  PUBLISHER = {Springer},
  YEAR      = {2005},
  EDITION   = {3rd}}
