isMulTorsionFree_iff_torsion_eq_bot

English

A commutative group G is torsion-free if and only if its torsion subgroup is trivial (equals ⊥).

Русский

Коммутативная группа G безторсионна тогда и только тогда, когда её торсионная подпгруппа тривиальна (равна ⊥).

LaTeX

$$$IsMulTorsionFree\ G \iff CommGroup.torsion G = \bot$$$

Lean4

@[to_additive]
theorem isMulTorsionFree_iff_torsion_eq_bot : IsMulTorsionFree G ↔ CommGroup.torsion G = ⊥ :=
  by
  rw [isMulTorsionFree_iff_not_isOfFinOrder, eq_bot_iff, SetLike.le_def]
  simp [not_imp_not, CommGroup.mem_torsion]

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