mem_zpowers_of_prime_card — Mathlib

English

In a group of prime order, every non-identity element generates the group; hence each element lies in zpowers g.

Русский

В группе простого порядка каждый ненулевой элемент порождает группу; следовательно, каждый элемент принадлежит zpowers g.

LaTeX

$$$|G| = p \Rightarrow (g \neq 1) \Rightarrow (g' \in zpowers(g))$$$

Lean4

@[to_additive]
theorem mem_zpowers_of_prime_card {p : ℕ} [hp : Fact p.Prime] (h : Nat.card G = p) {g g' : G} (hg : g ≠ 1) :
    g' ∈ zpowers g := by simp_rw [zpowers_eq_top_of_prime_card h hg, Subgroup.mem_top]

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