not_torsion_free — Mathlib

English

A nontrivial torsion group is not torsion-free.

Русский

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

LaTeX

$$$\forall G, \text{Not (IsTorsionFree } G)\iff \text{IsTorsion } G$$$

Lean4

/-- A nontrivial torsion group is not torsion-free. -/
@[to_additive (attr := deprecated not_isMulTorsionFree_of_isTorsion (since := "2025-04-23")) /--
    A nontrivial additive torsion group is not torsion-free. -/
    ]
theorem not_torsion_free [hN : Nontrivial G] : IsTorsion G → ¬IsTorsionFree G := fun tG =>
  not_isTorsionFree_iff.mpr <| by
    obtain ⟨x, hx⟩ := (nontrivial_iff_exists_ne (1 : G)).mp hN
    exact ⟨x, hx, tG x⟩

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