English
A nontrivial torsion group cannot be torsion-free.
Русский
Непустая торсионная группа не может быть безторсионной.
LaTeX
$$$\text{Not (IsTorsionFree G)} \Leftarrow (IsTorsion G) \to \text{Nontrivial } G$$$
Lean4
/-- A predicate on a monoid saying that only 1 is of finite order.
This definition is mathematically incorrect for monoids which are not groups.
Please use `IsMulTorsionFree` instead. -/
@[to_additive /-- A predicate on an additive monoid saying that only 0 is of finite order.
This definition is mathematically incorrect for monoids which are not groups.
Please use `IsAddTorsionFree` instead. -/
]
def IsTorsionFree :=
∀ g : G, g ≠ 1 → ¬IsOfFinOrder g
