zpowers_eq_top_of_prime_card — Mathlib

English

Any non-identity element of a finite group of prime order generates the group.

Русский

Любой ненулевой элемент конечной группы простого порядка порождает всю группу.

LaTeX

$$$|G| = p \text{ prime}, \ g \neq 1 \Rightarrow \langle g \rangle = G$$$

Lean4

/-- Any non-identity element of a finite group of prime order generates the group. -/
@[to_additive /-- Any non-identity element of a finite group of prime order generates the group. -/
    ]
theorem zpowers_eq_top_of_prime_card {p : ℕ} [hp : Fact p.Prime] (h : Nat.card G = p) {g : G} (hg : g ≠ 1) :
    zpowers g = ⊤ := by
  subst h
  have := (zpowers g).eq_bot_or_eq_top_of_prime_card
  rwa [zpowers_eq_bot, or_iff_right hg] at this

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