isCyclic_of_prime_card — Mathlib

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⟩

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