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 theorem is closely related to the Chinese Remainder theorem ([18]) and is a useful lemma to prove the basis theorem for finite abelian groups a...

Full description

Bibliographic Details
Main Authors: Arai Kenichi, Okazaki Hiroyuki, Shidama Yasunari
Format: Article
Language:English
Published: Sciendo 2012-12-01
Series:Formalized Mathematics
Online Access:https://doi.org/10.2478/v10037-012-0038-5