isTorsionFree_of_subsingleton — Mathlib

English

Subgroups of torsion-free groups are torsion-free.

Русский

Подгруппы безторсионных групп также безторционны.

LaTeX

$$$\text{IsTorsionFree} G \Rightarrow \text{Subgroup } H \Rightarrow \text{IsTorsionFree } H$$$

Lean4

@[to_additive (attr := deprecated Subsingleton.to_isMulTorsionFree (since := "2025-04-23"))]
theorem isTorsionFree_of_subsingleton [Subsingleton G] : IsTorsionFree G := fun _a ha _ => ha <| Subsingleton.elim _ _

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