isCyclic_of_card_pow_eq_one_le — Mathlib

English

A finite group of prime order is simple.

Русский

Конечная группа простого порядка простая.

LaTeX

$$IsSimpleGroup α$$

Lean4

@[to_additive isAddCyclic_of_card_nsmul_eq_zero_le,
  stacks 09HX "This theorem is stronger than \
      09HX. It removes the abelian condition, and requires only `≤` instead of `=`."]
theorem isCyclic_of_card_pow_eq_one_le : IsCyclic α :=
  have : Finset.Nonempty {a : α | orderOf a = Nat.card α} :=
    card_pos.1 <| by
      rw [Nat.card_eq_fintype_card, card_orderOf_eq_totient_aux₂ hn dvd_rfl, totient_pos]
      apply Fintype.card_pos
  let ⟨x, hx⟩ := this
  isCyclic_of_orderOf_eq_card x (Finset.mem_filter.1 hx).2

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