Mathlib Map

Theorems · Theorem · group theory

IsCyclic.exists_zpow_surjective

∀ {G : Type u} {inst : Pow G ℤ} [self : IsCyclic G], ∃ g, Function.Surjective fun x => g ^ x
Defined in
Mathlib.Algebra.Group.Defs
Cited by
3 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
IsCyclic
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

exists_zpow_surjective · cited by 3exists_zpow_surjectiveisAddCyclic_additive_iff · cited by 3isAddCyclic_additive_iffisCyclic_multiplicative_iff · cited by 0isCyclic_multiplicative_i…IsCyclic · cited by 122IsCyclicIsCyclic.exists_zpow_surjecti…CITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • IsCyclicstatement and proof · cited by 122

Cited by3

Results whose statement or proof uses this declaration.