subgroup — Mathlib

English

Subgroups of a torsion group are torsion groups.

Русский

Подгруппы тórсионной группы сами являются торсионными.

LaTeX

$$$\forall H\le G,\; IsTorsion(H)$, если $G$ удовлетворяет IsTorsion.$$

Lean4

/-- Subgroups of torsion groups are torsion groups. -/
@[to_additive /-- Subgroups of additive torsion groups are additive torsion groups. -/
    ]
theorem subgroup (tG : IsTorsion G) (H : Subgroup G) : IsTorsion H := fun h => Submonoid.isOfFinOrder_coe.1 <| tG h

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