isTorsion — Mathlib

English

If a group has a finite exponent, then the group is torsion.

Русский

Если существует конечный показатель порядка элементов группы, то группа торсиона.

LaTeX

$$$\exists n>0$ such that $g^n=e$ for all $g\in G$ implies IsTorsion(G).$$

Lean4

/-- If a group exponent exists, the group is torsion. -/
@[to_additive ExponentExists.is_add_torsion /-- If a group exponent exists, the group is additively torsion. -/
    ]
theorem isTorsion (h : ExponentExists G) : IsTorsion G := fun g =>
  by
  obtain ⟨n, npos, hn⟩ := h
  exact isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, hn g⟩

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