%0 Journal Article
%T Normal Subgroup of Product of Groups
%A Hiroyuki Okazaki
%A Kenichi Arai
%A Yasunari Shidama
%J Formalized Mathematics
%@ 1898-9934
%D 2011
%I 
%R 10.2478/v10037-011-0004-7
%X In [6] it was formalized that the direct product of a family of groups gives a new group. In this article, we formalize that for all j ¡Ê I, the group G = ¦°i¡ÊIGi has a normal subgroup isomorphic to Gj. Moreover, we show some relations between a family of groups and its direct product.
%U http://versita.metapress.com/content/kl04707085362l74/?p=25816f9e6d274cf5ab90abc2a2c39abd&pi=3