groupPowers — Mathlib

English

The submonoid generated by the powers of an element x is a group if x has finite order.

Русский

Подмножество порожденное степенями элемента x образует группу, если у x конечный порядок.

LaTeX

$$IsOfFinOrder x \\Rightarrow Group (Submonoid.powers x)$$

Lean4

/-- The submonoid generated by an element is a group if that element has finite order. -/
@[to_additive /-- The additive submonoid generated by an element is
    an additive group if that element has finite order. -/
    ]
noncomputable abbrev groupPowers (hx : IsOfFinOrder x) : Group (Submonoid.powers x) :=
  by
  obtain ⟨hpos, hx⟩ := hx.exists_pow_eq_one.choose_spec
  exact Submonoid.groupPowers hpos hx

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