English
For any G, x ∈ G, the set {x^i : i ∈ range(orderOf x)} equals the powers of x (cyclic subgroup generated by x).
Русский
Для элемента x ∈ G множество {x^i : i ∈ range(orderOf x)} равно циклической подгруппе, порождённой x.
LaTeX
$$$\{ x^i : i = 0,1,\dots, \operatorname{orderOf}(x)-1 \} = \langle x \rangle$$$
Lean4
@[to_additive]
theorem image_range_orderOf [DecidableEq G] :
letI : Fintype (zpowers x) := (Subgroup.zpowers x).instFintypeSubtypeMemOfDecidablePred
Finset.image (fun i => x ^ i) (Finset.range (orderOf x)) = (zpowers x : Set G).toFinset :=
by
letI : Fintype (zpowers x) := (Subgroup.zpowers x).instFintypeSubtypeMemOfDecidablePred
ext x
rw [Set.mem_toFinset, SetLike.mem_coe, mem_zpowers_iff_mem_range_orderOf]
/- TODO: Generalise to `Finite` + `CancelMonoid`. -/
