mem_powers_of_prime_card — Mathlib

English

Given Nat.card G = p prime, any non-identity element g has every element g' in Submonoid.powers g.

Русский

При Nat.card G = p простое, для любого g ≠ 1 каждый элемент лежит в Submonoid.powers g.

LaTeX

$$$Nat.card(G) = p \Rightarrow (g \neq 1) \Rightarrow (g' \in Submonoid.powers(g))$$$

Lean4

@[to_additive]
theorem mem_powers_of_prime_card {p : ℕ} [hp : Fact p.Prime] (h : Nat.card G = p) {g g' : G} (hg : g ≠ 1) :
    g' ∈ Submonoid.powers g :=
  by
  have : Finite G := Nat.finite_of_card_ne_zero (h ▸ hp.1.ne_zero)
  rw [mem_powers_iff_mem_zpowers]
  exact mem_zpowers_of_prime_card h hg

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