exists_monoid_generator — Mathlib

English

Let A be a finite cyclic group. There exists an element x in A such that every element of A is a power of x; equivalently, A = ⟨x⟩.

Русский

Пусть A — конечная циклическая группа. Существует элемент x ∈ A, такой что каждый элемент A можно записать как степень x; то есть A = ⟨x⟩.

LaTeX

$$$\exists x \in \alpha\; (\alpha = \langle x \rangle)$$$

Lean4

@[to_additive]
theorem exists_monoid_generator [Finite α] [IsCyclic α] : ∃ x : α, ∀ y : α, y ∈ Submonoid.powers x :=
  by
  simp_rw [mem_powers_iff_mem_zpowers]
  exact IsCyclic.exists_generator

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