English
A finite group of prime order is cyclic.
Русский
Конечная группа простого порядка циклична.
LaTeX
$$$[Finite(\\alpha)] \operatorname{card}(\\alpha) = p \implies IsCyclic(\\alpha)$$$
Lean4
/-- A finite group of prime order is cyclic. -/
@[to_additive /-- A finite group of prime order is cyclic. -/
]
theorem isCyclic_of_prime_card {p : ℕ} [hp : Fact p.Prime] (h : Nat.card α = p) : IsCyclic α :=
by
have : Finite α := Nat.finite_of_card_ne_zero (h ▸ hp.1.ne_zero)
have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp (h ▸ hp.1.one_lt)
obtain ⟨g, hg⟩ : ∃ g : α, g ≠ 1 := exists_ne 1
exact ⟨g, fun g' ↦ mem_zpowers_of_prime_card h hg⟩