English
The set of powers is finite iff a has finite order.
Русский
Множество степеней конечного элемента тогда и только тогда, когда у элемента конечный порядок.
LaTeX
$$Finite \left(\mathrm{powers}(a)\right) \iff \operatorname{IsOfFinOrder}(a)$$
Lean4
@[to_additive (attr := simp)]
theorem finite_powers : (powers a : Set G).Finite ↔ IsOfFinOrder a :=
by
refine ⟨fun h ↦ ?_, IsOfFinOrder.finite_powers⟩
obtain ⟨m, n, hmn, ha⟩ := h.exists_lt_map_eq_of_forall_mem (f := fun n : ℕ ↦ a ^ n) (fun n ↦ by simp [mem_powers_iff])
refine isOfFinOrder_iff_pow_eq_one.2 ⟨n - m, tsub_pos_iff_lt.2 hmn, ?_⟩
rw [← mul_left_cancel_iff (a := a ^ m), ← pow_add, add_tsub_cancel_of_le hmn.le, ha, mul_one]
