torsion — Mathlib

English

The torsion submonoid of a commutative monoid is torsion.

Русский

Торовая подплощадь коммутативного моноида является торсовой.

LaTeX

$$IsTorsion (torsion G)$$

Lean4

/-- The torsion submonoid of a commutative monoid.

(Note that by `Monoid.IsTorsion.group` torsion monoids are truthfully groups.)
-/
@[to_additive addTorsion /-- The torsion submonoid of an additive commutative monoid. -/
    ]
def torsion : Submonoid G where
  carrier := {x | IsOfFinOrder x}
  one_mem' := IsOfFinOrder.one
  mul_mem' hx hy := hx.mul hy

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