English
Quotienting a group by its torsion subgroup yields a torsion-free group.
Русский
Окружение группы по ее торсионной подпгруппе дает безторсионную группу.
LaTeX
$$$IsTorsionFree (HasQuotient.Quotient G (CommGroup.torsion G))$$$
Lean4
/-- Quotienting a group by its torsion subgroup yields a torsion-free group. -/
@[to_additive /-- Quotienting a group by its additive torsion subgroup yields an additive torsion-free group. -/
]
instance _root_.QuotientGroup.instIsMulTorsionFree : IsMulTorsionFree <| G ⧸ torsion G :=
by
refine .of_not_isOfFinOrder fun g hne hfin ↦ hne ?_
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⟩)
