<abstract xmlns="http://www.w3.org/1999/xhtml"><p>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.</p></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.

Isomorphisms of Direct Products of Finite Cyclic Groups

Tokyo University of Science, Chiba, Japan

Formalized Mathematics

{"article-title":"Isomorphisms of Direct Products of Finite Cyclic Groups"}

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

Isomorphisms of Direct Products of Finite Cyclic Groups

Online veröffentlicht: 02. Feb. 2013

Seitenbereich: 343 - 347

DOI: https://doi.org/10.2478/v10037-012-0038-5

This content is open access.