Normal Subgroup of Product of Groups

Hiroyuki Okazaki; Kenichi Arai; Yasunari Shidama

Formalized Mathematics (2011)

  • Volume: 19, Issue: 1, page 23-26
  • ISSN: 1426-2630

Abstract

top
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.

How to cite

top

Hiroyuki Okazaki, Kenichi Arai, and Yasunari Shidama. "Normal Subgroup of Product of Groups." Formalized Mathematics 19.1 (2011): 23-26. <http://eudml.org/doc/266892>.

@article{HiroyukiOkazaki2011,
abstract = {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.},
author = {Hiroyuki Okazaki, Kenichi Arai, Yasunari Shidama},
journal = {Formalized Mathematics},
keywords = {direct products of groups; direct sums; normal subgroups},
language = {eng},
number = {1},
pages = {23-26},
title = {Normal Subgroup of Product of Groups},
url = {http://eudml.org/doc/266892},
volume = {19},
year = {2011},
}

TY - JOUR
AU - Hiroyuki Okazaki
AU - Kenichi Arai
AU - Yasunari Shidama
TI - Normal Subgroup of Product of Groups
JO - Formalized Mathematics
PY - 2011
VL - 19
IS - 1
SP - 23
EP - 26
AB - 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.
LA - eng
KW - direct products of groups; direct sums; normal subgroups
UR - http://eudml.org/doc/266892
ER -

References

top
  1. [1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  2. [2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990. 
  3. [3] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Formalized Mathematics, 5(4):485-492, 1996. 
  4. [4] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990. 
  5. [5] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  6. [6] Artur Korniłowicz. The product of the families of the groups. Formalized Mathematics, 7(1):127-134, 1998. Zbl1298.55008
  7. [7] Wojciech A. Trybulec. Classes of conjugation. Normal subgroups. Formalized Mathematics, 1(5):955-962, 1990. 
  8. [8] Wojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821-827, 1990. 
  9. [9] Wojciech A. Trybulec. Subgroup and cosets of subgroups. Formalized Mathematics, 1(5):855-864, 1990. 
  10. [10] Wojciech A. Trybulec. Lattice of subgroups of a group. Frattini subgroup. Formalized Mathematics, 2(1):41-47, 1991. 
  11. [11] Wojciech A. Trybulec and Michał J. Trybulec. Homomorphisms and isomorphisms of groups. Quotient group. Formalized Mathematics, 2(4):573-578, 1991. 
  12. [12] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  13. [13] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.