torsion_int — Mathlib

English

The integer torsion of an abelian group equals the usual additive torsion subgroup.

Русский

Целочисленная торсия абелевой группы равна обычной подгруппе торсии.

LaTeX

$$torsion Z G = AddCommGroup.torsion G$$

Lean4

theorem torsion_int {G} [AddCommGroup G] : (torsion ℤ G).toAddSubgroup = AddCommGroup.torsion G :=
  by
  ext x
  refine ((isOfFinAddOrder_iff_zsmul_eq_zero (x := x)).trans ?_).symm
  simp [mem_nonZeroDivisors_iff_ne_zero]

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