English
For groups M and N, the product M × N is cyclic iff both M and N are cyclic and their orders are coprime.
Русский
Для групп M и N произведение M × N циклическое тогда и только тогда, когда обе группы циклические и их порядки взаимно просты.
LaTeX
$$IsCyclic(M × N) \iff IsCyclic(M) ∧ IsCyclic(N) ∧ gcd(card M, card N) = 1$$
Lean4
/-- The product of two finite groups is cyclic iff
both of them are cyclic and their orders are coprime. -/
@[to_additive AddGroup.isAddCyclic_prod_iff /-- The product of two finite additive groups is cyclic
iff both of them are cyclic and their orders are coprime. -/
]
theorem isCyclic_prod_iff {M N : Type*} [Group M] [Group N] :
IsCyclic (M × N) ↔ IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N) :=
by
refine ⟨fun h ↦ ⟨isCyclic_left_of_prod M N, isCyclic_right_of_prod M N, ?_⟩, fun ⟨hM, hN, h⟩ ↦ ?_⟩
· cases (finite_or_infinite M).symm
· cases subsingleton_or_nontrivial N; · simp
exact (not_isCyclic_prod_of_infinite_nontrivial M N h).elim
cases (finite_or_infinite N).symm
· cases subsingleton_or_nontrivial M; · simp
rw [(MulEquiv.prodComm ..).isCyclic] at h
exact (not_isCyclic_prod_of_infinite_nontrivial N M h).elim
apply coprime_card_of_isCyclic_prod
· let f := MonoidHom.snd M N
let e : f.ker ≃* M := by
rw [MonoidHom.ker_snd]
exact ((Subgroup.prodEquiv ..).trans .prodUnique).trans Subgroup.topEquiv
let _ := hM.commGroup; let _ := hN.commGroup
rw [← e.isCyclic] at hM
rw [← Nat.card_congr e.toEquiv] at h
exact isCyclic_of_coprime_card_ker f h Prod.snd_surjective
