Theorems · Theorem · order theory

Subgroup.cyclic_of_min

∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G}
  {a : G}, IsLeast {g | g ∈ H ∧ 1 < g} a → H = Subgroup.closure {a}

Given a subgroup H of a decidable linearly ordered mul-archimedean abelian group G, if there exists a minimal element a of H ∩ G_{>1} then H is generated by a.

Defined in

Mathlib.GroupTheory.Archimedean

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommGroupLinearOrderIsOrderedMonoidMulArchimedean