subgroup — Mathlib

English

Subgroups of torsion-free groups are torsion-free.

Русский

Подгруппы безторсионных групп являются безторсионными.

LaTeX

$$$\text{IsTorsionFree } G \Rightarrow \forall H \le G, \text{IsTorsionFree } H$$$

Lean4

/-- Subgroups of torsion-free groups are torsion-free. -/
@[to_additive (attr := deprecated Subgroup.instIsMulTorsionFree (since := "2025-04-23")) /--
    Subgroups of additive torsion-free groups are additively torsion-free. -/
    ]
theorem subgroup (tG : IsTorsionFree G) (H : Subgroup G) : IsTorsionFree H := fun h hne ↦
  Submonoid.isOfFinOrder_coe.not.1 <| tG h <| by norm_cast

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