powers_eq_image_range_orderOf — Mathlib

English

If x has finite order, the set of its powers equals the image of the range of ord(x) under k ↦ x^k.

Русский

Если ord(x) конечен, то множество степеней x совпадает с образов диапазона ord(x) под отображением k ↦ x^k.

LaTeX

$$$ \forall G [Monoid G], \forall x : G, IsOfFinOrder x → (\text{powers}(x) = \{ x^k : 0 \le k < ord(x) \})$$$

Lean4

@[to_additive]
protected theorem powers_eq_image_range_orderOf [DecidableEq G] (hx : IsOfFinOrder x) :
    (Submonoid.powers x : Set G) = (Finset.range (orderOf x)).image (x ^ ·) :=
  Set.ext fun _ ↦ hx.mem_powers_iff_mem_range_orderOf

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