Isomorphisms of Direct Products of Finite Cyclic Groups

Kenichi Arai; Hiroyuki Okazaki; Yasunari Shidama

Formalized Mathematics (2012)

  • Volume: 20, Issue: 4, page 343-347
  • ISSN: 1426-2630

Abstract

top
In this article, we formalize that every finite cyclic group is isomorphic to a direct product of finite cyclic groups which orders are relative prime. This theorem is closely related to the Chinese Remainder theorem ([18]) and is a useful lemma to prove the basis theorem for finite abelian groups and the fundamental theorem of finite abelian groups. Moreover, we formalize some facts about the product of a finite sequence of abelian groups.

How to cite

top

Kenichi Arai, Hiroyuki Okazaki, and Yasunari Shidama. "Isomorphisms of Direct Products of Finite Cyclic Groups." Formalized Mathematics 20.4 (2012): 343-347. <http://eudml.org/doc/267547>.

@article{KenichiArai2012,
abstract = {In this article, we formalize that every finite cyclic group is isomorphic to a direct product of finite cyclic groups which orders are relative prime. This theorem is closely related to the Chinese Remainder theorem ([18]) and is a useful lemma to prove the basis theorem for finite abelian groups and the fundamental theorem of finite abelian groups. Moreover, we formalize some facts about the product of a finite sequence of abelian groups.},
author = {Kenichi Arai, Hiroyuki Okazaki, Yasunari Shidama},
journal = {Formalized Mathematics},
keywords = {formalized mathematics; finite cyclic groups; finite Abelian groups; direct products},
language = {eng},
number = {4},
pages = {343-347},
title = {Isomorphisms of Direct Products of Finite Cyclic Groups},
url = {http://eudml.org/doc/267547},
volume = {20},
year = {2012},
}

TY - JOUR
AU - Kenichi Arai
AU - Hiroyuki Okazaki
AU - Yasunari Shidama
TI - Isomorphisms of Direct Products of Finite Cyclic Groups
JO - Formalized Mathematics
PY - 2012
VL - 20
IS - 4
SP - 343
EP - 347
AB - In this article, we formalize that every finite cyclic group is isomorphic to a direct product of finite cyclic groups which orders are relative prime. This theorem is closely related to the Chinese Remainder theorem ([18]) and is a useful lemma to prove the basis theorem for finite abelian groups and the fundamental theorem of finite abelian groups. Moreover, we formalize some facts about the product of a finite sequence of abelian groups.
LA - eng
KW - formalized mathematics; finite cyclic groups; finite Abelian groups; direct products
UR - http://eudml.org/doc/267547
ER -

References

top
  1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990. 
  2. [2] Grzegorz Bancerek. K¨onig’s theorem. Formalized Mathematics, 1(3):589-593, 1990. 
  3. [3] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  4. [4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990. 
  5. [5] Czesław Bylinski. Binary operations. Formalized Mathematics, 1(1):175-180, 1990. 
  6. [6] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990. 
  7. [7] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  8. [8] Czesław Bylinski. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  9. [9] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  10. [10] Czesław Bylinski. The sum and product of finite sequences of real numbers. FormalizedMathematics, 1(4):661-668, 1990. 
  11. [11] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990. 
  12. [12] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5):841-845, 1990. 
  13. [13] Artur Korniłowicz. On the real valued functions. Formalized Mathematics, 13(1):181-187, 2005. 
  14. [14] Eugeniusz Kusak, Wojciech Leonczuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990. 
  15. [15] Anna Lango and Grzegorz Bancerek. Product of families of groups and vector spaces. Formalized Mathematics, 3(2):235-240, 1992. 
  16. [16] Hiroyuki Okazaki, Noboru Endou, and Yasunari Shidama. Cartesian products of family of real linear spaces. Formalized Mathematics, 19(1):51-59, 2011, doi: 10.2478/v10037-011-0009-2.[Crossref] Zbl1276.46015
  17. [17] Christoph Schwarzweller. The ring of integers, Euclidean rings and modulo integers. Formalized Mathematics, 8(1):29-34, 1999. 
  18. [18] Christoph Schwarzweller. Modular integer arithmetic. Formalized Mathematics, 16(3):247-252, 2008, doi:10.2478/v10037-008-0029-8.[Crossref] 
  19. [19] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4):341-347, 2003. 
  20. [20] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990. 
  21. [21] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990. 
  22. [22] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  23. [23] 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.