isCyclic_iff_exists_orderOf_eq_natCard

English

For a finite group α, α is cyclic iff there exists an element g with orderOf g = card α.

Русский

Для конечной группы α она циклична тогда и только тогда, когда существует элемент g such that orderOf(g) = card(α).

LaTeX

$$$[Finite(\\alpha)] : IsCyclic(\\alpha) \\Leftrightarrow \exists g : \\alpha, \\operatorname{orderOf}(g) = |\\alpha|$$$

Lean4

@[to_additive]
theorem isCyclic_iff_exists_orderOf_eq_natCard [Finite α] : IsCyclic α ↔ ∃ g : α, orderOf g = Nat.card α := by
  simp_rw [isCyclic_iff_exists_zpowers_eq_top, ← card_eq_iff_eq_top, Nat.card_zpowers]

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