not_torsion — Mathlib

English

Not (IsTorsion G) when G is trivial implies not torsion-free.

Русский

Не торсионность предиката указывает на то, что группу нельзя считать безторсионной.

LaTeX

$$$\text{Not (IsTorsion G)} \Rightarrow ...$$$

Lean4

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

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