English
If M is infinite and N is nontrivial, then the additive product M × N is not cyclic.
Русский
Если M бесконечна, а N нечтожна, то их прямое произведение в аддитивной структуре не циклично.
LaTeX
$$Infinite M \land Nontrivial N \Rightarrow \neg IsAddCyclic(M \times N)$$
Lean4
theorem not_isAddCyclic_prod_of_infinite_nontrivial (M N : Type*) [AddGroup M] [AddGroup N] [Infinite M]
[Nontrivial N] : ¬IsAddCyclic (M × N) := fun hMN ↦
by
rw [←
((zmodAddCyclicAddEquiv <| isAddCyclic_left_of_prod M N).prodCongr
(zmodAddCyclicAddEquiv <| isAddCyclic_right_of_prod M N)).isAddCyclic,
Nat.card_eq_zero_of_infinite] at hMN
cases (finite_or_infinite N).symm
· rw [Nat.card_eq_zero_of_infinite] at hMN
let f := (ZMod.castHom (dvd_zero _) (ZMod 2)).toAddMonoidHom
have hf := ZMod.castHom_surjective (dvd_zero 2)
have := isAddCyclic_of_surjective (f.prodMap f) (Prod.map_surjective.mpr ⟨hf, hf⟩)
simpa using coprime_card_of_isAddCyclic_prod (ZMod 2) (ZMod 2)
let ZN := ZMod (Nat.card N)
have : NeZero (Nat.card N) := ⟨Nat.card_pos.ne'⟩
have :=
isAddCyclic_of_surjective ((ZMod.castHom (dvd_zero _) ZN).toAddMonoidHom.prodMap (.id ZN))
(Prod.map_surjective.mpr ⟨ZMod.castHom_surjective (dvd_zero _), Function.surjective_id⟩)
exact Finite.one_lt_card (α := N).ne' (by simpa [ZN] using coprime_card_of_isAddCyclic_prod ZN ZN)
