powers_eq_top_of_prime_card — Mathlib

English

In a group of prime order, the powers of any non-identity element generate the whole group.

Русский

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

LaTeX

$$$|G| = p \text{ prime}, g \neq 1 \Rightarrow Submonoid.powers(g) = G$$$

Lean4

@[to_additive]
theorem powers_eq_top_of_prime_card {p : ℕ} [hp : Fact p.Prime] (h : Nat.card G = p) {g : G} (hg : g ≠ 1) :
    Submonoid.powers g = ⊤ := by
  ext x
  simp [mem_powers_of_prime_card h hg]

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