Theorems · Theorem · order theory

AddSubgroup.cyclic_of_min

∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G]
  {H : AddSubgroup G} {a : G}, IsLeast {g | g ∈ H ∧ 0 < g} a → H = AddSubgroup.closure {a}

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

Defined in

Mathlib.GroupTheory.Archimedean

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidArchimedean