Theorems · Theorem · group theory

LinearOrderedCommGroup.Subgroup.genLTOne_unique

∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedMonoid G] (H : Subgroup G)
  [inst_3 : Nontrivial ↥H] [hH : IsCyclic ↥H] {g : G},
  g < 1 → Subgroup.zpowers g = H → g = LinearOrderedCommGroup.Subgroup.genLTOne H

Defined in

Mathlib.Algebra.Order.Group.Cyclic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommGroupLinearOrderIsOrderedMonoidNontrivialIsCyclic