orderOf_eq_card_of_zpowers_eq_top

English

In a cyclic group, for any k ≠ 0 with k < card G, there exists a such that a^k ≠ 1.

Русский

В циклической группе для любого k ≠ 0 с k < |G| существует a, такое что a^k ≠ 1.

LaTeX

$$∃ a : G, a^k ≠ 1, when k ≠ 0 and k < Nat.card G$$

Lean4

@[to_additive]
theorem orderOf_eq_card_of_zpowers_eq_top {g : G} (h : Subgroup.zpowers g = ⊤) : orderOf g = Nat.card G :=
  orderOf_eq_card_of_forall_mem_zpowers fun _ ↦ h.ge (Subgroup.mem_top _)

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