exists_ofOrder_eq_natCard — Mathlib

English

Let A be a finite cyclic group. There exists g ∈ A with order(g) = |A|.

Русский

Пусть A — конечная циклическая группа. Существует элемент g ∈ A, чей порядок равенcardinality A.

LaTeX

$$$\exists g \in \alpha,\ \mathrm{orderOf}(g) = |\alpha|$$$

Lean4

@[to_additive]
theorem exists_ofOrder_eq_natCard [h : IsCyclic α] : ∃ g : α, orderOf g = Nat.card α :=
  by
  obtain ⟨g, hg⟩ := h.exists_generator
  use g
  rw [← card_zpowers g, (eq_top_iff' (zpowers g)).mpr hg]
  exact Nat.card_congr (Equiv.Set.univ α)

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