mem_zpowers_iff_mem_range_orderOf

English

For a finite group G, the membership in powers x is equivalent to membership in zpowers x.

Русский

Для конечной группы G принадлежность к powers x эквивалентна принадлежности к zpowers x.

LaTeX

$$mem_powers_iff_mem_zpowers : y ∈ powers x ↔ y ∈ zpowers x$$

Lean4

@[to_additive]
theorem mem_zpowers_iff_mem_range_orderOf [DecidableEq G] :
    y ∈ zpowers x ↔ y ∈ (Finset.range (orderOf x)).image (x ^ ·) :=
  (isOfFinOrder_of_finite _).mem_zpowers_iff_mem_range_orderOf

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