mem_powers_iff_mem_range_orderOf — Mathlib

English

Let G be a finite left-cancellative monoid and x,y ∈ G. Then y belongs to the powers of x if and only if y belongs to the image of x^i for i in the range 0 to orderOf(x)−1.

Русский

Пусть G — конечный левоконечный моноид, и x,y ∈ G. Тогда y ∈ powers(x) тогда и только тогда, когда y ∈ { x^i : 0 ≤ i < orderOf(x) }.

LaTeX

$$$y \in \text{powers}(x) \iff y \in (\text{range}(\operatorname{orderOf}(x))).image (x^{\cdot})$$$

Lean4

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

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