eq_bot_or_eq_top_of_prime_card — Mathlib

English

If H is a subgroup of G and card G is prime, then H is either {e} or G.

Русский

Если H ≤ G и card(G) — простое число, то H = {e} или H = G.

LaTeX

$$$H = \{e\} \\lor H = G$ whenever $|G|$ is prime.$$

Lean4

@[to_additive]
theorem eq_bot_or_eq_top_of_prime_card (H : Subgroup G) [hp : Fact (Nat.card G).Prime] : H = ⊥ ∨ H = ⊤ :=
  by
  have : Finite G := Nat.finite_of_card_ne_zero hp.1.ne_zero
  have := card_subgroup_dvd_card H
  rwa [Nat.dvd_prime hp.1, ← eq_bot_iff_card, card_eq_iff_eq_top] at this

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