Archimedean groups

This file proves a few facts about ordered groups which satisfy the Archimedean property, that is: class Archimedean (α) [OrderedAddCommMonoid α] : Prop := (arch : ∀ (x : α) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y)

They are placed here in a separate file (rather than incorporated as a continuation of Algebra.Order.Archimedean) because they rely on some imports from GroupTheory -- bundled subgroups in particular.

The main result is AddSubgroup.zmultiples_eq_of_isLeast_mem_and_pos: A subgroup of a decidable archimedean abelian group is cyclic, if its set of positive elements has a minimal element.

The file also supports multiplicative groups via MulArchimedean.

The result is also used in Topology.Instances.Real as an ingredient in the classification of subgroups of ℝ.

theorem Subgroup.zpowers_eq_of_isLeast_mem_and_one_lt {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G} {a : G} (ha : IsLeast {g : G | g ∈ H ∧ 1 < g} a) : zpowers a = H

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.

theorem AddSubgroup.zmultiples_eq_of_isLeast_mem_and_pos {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {H : AddSubgroup G} {a : G} (ha : IsLeast {g : G | g ∈ H ∧ 0 < g} a) : zmultiples a = H

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.

@[deprecated Subgroup.zpowers_eq_of_isLeast_mem_and_one_lt (since := "2026-08-30")]

theorem Subgroup.cyclic_of_min {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G} {a : G} (ha : IsLeast {g : G | g ∈ H ∧ 1 < g} a) : zpowers a = H

Alias of Subgroup.zpowers_eq_of_isLeast_mem_and_one_lt.

---

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.

@[deprecated AddSubgroup.zmultiples_eq_of_isLeast_mem_and_pos (since := "2026-08-30")]

theorem AddSubgroup.cyclic_of_min {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {H : AddSubgroup G} {a : G} (ha : IsLeast {g : G | g ∈ H ∧ 0 < g} a) : zmultiples a = H

Alias of AddSubgroup.zmultiples_eq_of_isLeast_mem_and_pos.

---

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.

theorem Subgroup.exists_isLeast_one_lt {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G} (hbot : H ≠ ⊥) {a : G} (h₀ : 1 < a) (hd : Disjoint (↑H) (Set.Ioo 1 a)) : ∃ (b : G), IsLeast {g : G | g ∈ H ∧ 1 < g} b

If a nontrivial subgroup of a linear ordered commutative group is disjoint with the interval Set.Ioo 1 a for some 1 < a, then the set of elements greater than 1 of this group admits the least element.

theorem AddSubgroup.exists_isLeast_pos {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {H : AddSubgroup G} (hbot : H ≠ ⊥) {a : G} (h₀ : 0 < a) (hd : Disjoint (↑H) (Set.Ioo 0 a)) : ∃ (b : G), IsLeast {g : G | g ∈ H ∧ 0 < g} b

If a nontrivial additive subgroup of a linear ordered additive commutative group is disjoint with the interval Set.Ioo 0 a for some positive a, then the set of positive elements of this group admits the least element.