Group_Direct_Product_of_Cyclic_Groups_v2
Provedcoprimecyclicdirect-productgroup-theoryproofwiki
The direct product of cyclic groups Z_n and Z_m is cyclic if and only if gcd(n, m) = 1.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.GroupTheory.SpecificGroups.Cyclic import Mathlib.Data.ZMod.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.GroupTheory.SpecificGroups.Cyclic import Mathlib.Data.ZMod.Basic theorem Group_Direct_Product_of_Cyclic_Groups_v2 (n m : ℕ) (hn : 0 < n) (hm : 0 < m) (hcop : Nat.Coprime n m) : IsAddCyclic (ZMod n × ZMod m) := by sorry
Source