English
Quotienting a group by its torsion subgroup yields a torsion-free group (alternate naming).
Русский
Квазиобразование группы по её торсионной подпгруппе дает безторсионную группу.
LaTeX
$$$IsTorsionFree (HasQuotient.Quotient G (CommGroup.torsion G))$$$
Lean4
/-- Quotienting a group by its torsion subgroup yields a torsion free group. -/
@[to_additive (attr := deprecated QuotientGroup.instIsMulTorsionFree (since := "2025-04-23")) /--
Quotienting a group by its additive torsion subgroup yields an additive torsion free group. -/
]
theorem quotient_torsion : IsTorsionFree <| G ⧸ torsion G := fun g hne hfin =>
hne <| by
obtain ⟨g⟩ := g
obtain ⟨m, mpos, hm⟩ := hfin.exists_pow_eq_one
obtain ⟨n, npos, hn⟩ := ((QuotientGroup.eq_one_iff _).mp hm).exists_pow_eq_one
exact
(QuotientGroup.eq_one_iff g).mpr
(isOfFinOrder_iff_pow_eq_one.mpr ⟨m * n, mul_pos mpos npos, (pow_mul g m n).symm ▸ hn⟩)
