Group_Direct_Product_of_Infinite_Cyclic_Groups_v2
Provedcyclicdirect-productgroup-theoryproofwiki
The direct product of two infinite cyclic groups (Z × Z) is not cyclic.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Group_Direct_Product_of_Infinite_Cyclic_Groups_v2 : ¬ IsAddCyclic (ℤ × ℤ) := by sorry
Source