not_isCyclic_prod_of_infinite_nontrivial

English

If M is infinite and N is nontrivial, then the (multiplicative) product M × N is not cyclic.

Русский

Если M бесконечна, а N непустая, то их произведение не циклично.

LaTeX

$$Infinite M \land Nontrivial N \Rightarrow \neg IsCyclic(M \times N)$$

Lean4

@[to_additive existing not_isAddCyclic_prod_of_infinite_nontrivial]
theorem not_isCyclic_prod_of_infinite_nontrivial (M N : Type*) [Group M] [Group N] [Infinite M] [Nontrivial N] :
    ¬IsCyclic (M × N) :=
  by
  rw [← isAddCyclic_additive_iff, (AddEquiv.prodAdditive ..).isAddCyclic]
  apply not_isAddCyclic_prod_of_infinite_nontrivial

Похожие утверждения