Theorems · Theorem · order theory

Subgroup.mem_closure_singleton_iff_existsUnique_zpow

∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b : G},
  a ≠ 1 → (b ∈ Subgroup.closure {a} ↔ ∃! k, a ^ k = b)

The subgroup generated by an element of a group equals the set of integer powers of the element, such that each power is a unique element. This is the stronger version of Subgroup.mem_closure_singleton.

Defined in

Mathlib.GroupTheory.ArchimedeanDensely

Cited by

0 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommGroupLinearOrderIsOrderedMonoid