isCyclic_iff_exists_natCard_le_orderOf

English

For a finite group α, α is cyclic iff there exists g with Nat.card α ≤ orderOf g.

Русский

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

LaTeX

$$$[Finite(\\alpha)] \\Leftrightarrow \exists g : \\alpha, Nat.card(\\alpha) \\le orderOf(g)$$$

Lean4

@[to_additive]
theorem isCyclic_iff_exists_natCard_le_orderOf [Finite α] : IsCyclic α ↔ ∃ g : α, Nat.card α ≤ orderOf g :=
  by
  rw [isCyclic_iff_exists_orderOf_eq_natCard]
  apply exists_congr
  intro g
  exact ⟨Eq.ge, le_antisymm orderOf_le_card⟩

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