not_isMulTorsionFree_iff_isOfFinOrder

English

The negation of IsMulTorsionFree is equivalent to the existence of an element a ≠ 1 with IsOfFinOrder a.

Русский

Утверждение против IsMulTorsionFree эквивалентно существованию элемента a ≠ 1 с IsOfFinOrder a.

LaTeX

$$¬IsMulTorsionFree G ⇔ ∃ a ≠ 1, IsOfFinOrder a$$

Lean4

@[to_additive]
theorem not_isMulTorsionFree_iff_isOfFinOrder : ¬IsMulTorsionFree G ↔ ∃ a ≠ (1 : G), IsOfFinOrder a := by
  simp [isMulTorsionFree_iff_not_isOfFinOrder]

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