isSimpleGroup_of_prime_card — Mathlib

English

If α is a finite group of prime order p, then α is simple.

Русский

Если группа α конечна и имеет порядок p, где p простое, то она простая.

LaTeX

$$IsSimpleGroup α$$

Lean4

/-- A finite group of prime order is simple. -/
@[to_additive /-- A finite group of prime order is simple. -/
    ]
theorem isSimpleGroup_of_prime_card {p : ℕ} [hp : Fact p.Prime] (h : Nat.card α = p) : IsSimpleGroup α :=
  by
  subst h
  have : Finite α := Nat.finite_of_card_ne_zero hp.1.ne_zero
  have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp hp.1.one_lt
  exact ⟨fun H _ => H.eq_bot_or_eq_top_of_prime_card⟩

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