orderOf_eq_card_powers — Mathlib

English

In a finite group G, the order of x equals the number of elements in the set of powers of x.

Русский

В конечной группе G порядок элемента x равен числу элементов множества степеней x.

LaTeX

$$\operatorname{orderOf}(x) = \lvert \text{powers}(x) \rvert$$

Lean4

@[to_additive]
theorem orderOf_eq_card_powers : orderOf x = Fintype.card (powers x : Submonoid G) :=
  (Fintype.card_fin (orderOf x)).symm.trans <| Fintype.card_eq.2 ⟨finEquivPowers <| isOfFinOrder_of_finite _⟩

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