finite_zpowers — Mathlib

English

The finiteness of the underlying subgroup of z-powers is equivalent to a being of finite order.

Русский

Конечность подгруппы z-пowers эквивалентна тому, что a имеет конечный порядок.

LaTeX

$$$ (\mathrm{zpowers}(a) \text{ as a set }).Finite \iff \mathrm{IsOfFinOrder}(a) $$$

Lean4

@[to_additive (attr := simp)]
theorem finite_zpowers : (zpowers a : Set α).Finite ↔ IsOfFinOrder a := by
  simp only [← orderOf_pos_iff, ← Nat.card_zpowers, Nat.card_pos_iff, ← SetLike.coe_sort_coe, nonempty_coe_sort,
    Nat.card_pos_iff, Set.finite_coe_iff, Subgroup.coe_nonempty, true_and]

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