torsion_eq_torsion_submonoid — Mathlib

English

The torsion submonoid of an abelian group equals the torsion subgroup viewed as a submonoid.

Русский

Торсионная подмонадa абелевой группы равна торсионной подпгруппе, взятой как подмоноид.

LaTeX

$$$CommMonoid.torsion G = (torsion G).toSubmonoid$$$

Lean4

/-- The torsion submonoid of an abelian group equals the torsion subgroup as a submonoid. -/
@[to_additive add_torsion_eq_add_torsion_submonoid /--
    The additive torsion submonoid of an abelian group equals the torsion
          subgroup as a submonoid. -/
    ]
theorem torsion_eq_torsion_submonoid : CommMonoid.torsion G = (torsion G).toSubmonoid :=
  rfl

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