not_isTorsionFree_iff — Mathlib

English

A nontrivial torsion-free group is not torsion.

Русский

Не пустая безторсионная группа не является торсионной.

LaTeX

$$$\text{Not (IsTorsion G)} \Leftarrow (IsTorsionFree G) \to \text{Not torsion}$$$

Lean4

/-- A nontrivial monoid is not torsion-free if any nontrivial element has finite order. -/
@[to_additive (attr := deprecated not_isMulTorsionFree_iff_isOfFinOrder (since := "2025-04-23")) /--
    An additive monoid is not torsion free if any nontrivial element has finite order. -/
    ]
theorem not_isTorsionFree_iff : ¬IsTorsionFree G ↔ ∃ g : G, g ≠ 1 ∧ IsOfFinOrder g := by
  simp_rw [IsTorsionFree, Ne, not_forall, Classical.not_not, exists_prop]

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