mem_powers_iff_mem_range_orderOf — Mathlib

English

If x has finite order, then a group element y lies in the powers of x if and only if y equals x^k for some k within 0 ≤ k < ord(x).

Русский

Если элемент x имеет конечный порядок, то элемент y принадлежит степеням x тогда и только тогда, когда y = x^k для некоторого k в диапазоне 0 ≤ k < ord(x).

LaTeX

$$$ \forall G [Monoid G], \forall x,y : G, IsOfFinOrder x → (y \in \text{powers}(x) \leftrightarrow \exists k < ord(x), y = x^k)$$$

Lean4

@[to_additive]
protected theorem mem_powers_iff_mem_range_orderOf [DecidableEq G] (hx : IsOfFinOrder x) :
    y ∈ Submonoid.powers x ↔ y ∈ (Finset.range (orderOf x)).image (x ^ ·) :=
  Finset.mem_range_iff_mem_finset_range_of_mod_eq' hx.orderOf_pos <| pow_mod_orderOf _

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