exists_zpow_surjective — Mathlib

English

Let G be cyclic with Pow G ℤ. Then there exists g ∈ G such that the map x ↦ g^x (x ∈ ℤ) is surjective onto G.

Русский

Пусть G циклично и имеется возведение в целые степени. Существует элемент g ∈ G, для которого отображение x ↦ g^x (x ∈ ℤ) сюръективно на G.

LaTeX

$$$\\exists g \\in G, \\operatorname{Surjective}(x \\mapsto g^{x} : \\mathbb{Z} \\to G)$$$

Lean4

@[to_additive]
theorem exists_zpow_surjective (G : Type*) [Pow G ℤ] [IsCyclic G] : ∃ g : G, Function.Surjective (g ^ · : ℤ → G) :=
  IsCyclic.exists_zpow_surjective

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