isCyclic_of_card_le_orderOf — Mathlib

English

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

Русский

Для конечной группы α IsCyclic α эквивалентно существованию элемента g с Nat.card α ≤ orderOf g.

LaTeX

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

Lean4

@[to_additive]
theorem isCyclic_of_card_le_orderOf [Finite α] (x : α) (hx : Nat.card α ≤ orderOf x) : IsCyclic α :=
  isCyclic_iff_exists_natCard_le_orderOf.mpr ⟨x, hx⟩

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