isTorsionFree_iff_torsion_eq_bot — Mathlib

English

In a commutative group, IsTorsionFree G is equivalent to torsion G = ⊥.

Русский

В коммутативной группе IsTorsionFree G эквивалентно torsion G = ⊥.

LaTeX

$$$IsTorsionFree\ G \iff CommGroup.torsion G = \bot$$$

Lean4

@[to_additive (attr := deprecated CommGroup.isMulTorsionFree_iff_torsion_eq_bot (since := "2025-04-23"))]
theorem isTorsionFree_iff_torsion_eq_bot {G} [CommGroup G] : IsTorsionFree G ↔ CommGroup.torsion G = ⊥ :=
  by
  rw [IsTorsionFree, eq_bot_iff, SetLike.le_def]
  simp [not_imp_not, CommGroup.mem_torsion]

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