isCyclic_of_orderOf_eq_card — Mathlib

English

If α is finite and there exists x with orderOf x = card α, then α is cyclic.

Русский

Если α конечна и существует x such that orderOf(x) = card α, то α циклична.

LaTeX

$$$[Finite(\\alpha)] (x : \\alpha) (orderOf(x) = Nat.card(\\alpha)) \Rightarrow IsCyclic(\\alpha)$$$

Lean4

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

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