Archimedean groups are either discrete or densely ordered

This file proves a few additional facts about linearly ordered additive groups which satisfy the Archimedean property -- they are either order-isomorphic and additively isomorphic to the integers, or they are densely ordered.

They are placed here in a separate file (rather than incorporated as a continuation of GroupTheory.Archimedean) because they rely on some imports from pointwise lemmas.

theorem exists_pow_lt₀ {G : Type u_1} [LinearOrderedCommGroupWithZero G] [MulArchimedean G] {a : G} (ha : a < 1) (b : Gˣ) : ∃ (n : ℕ), a ^ n < ↑b

theorem Subgroup.mem_zpowers_iff_existsUnique_zpow {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b : G} (ha : a ≠ 1) : b ∈ zpowers 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.

theorem AddSubgroup.mem_zmultiples_iff_existsUnique_zsmul {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (ha : a ≠ 0) : b ∈ zmultiples a ↔ ∃! k : ℤ, k • a = b

The additive subgroup generated by an element of an additive group equals the set of integer multiples of the element, such that each multiple is a unique element. This is the stronger version of AddSubgroup.mem_closure_singleton.

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

theorem Subgroup.mem_closure_singleton_iff_existsUnique_zpow {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b : G} (ha : a ≠ 1) : b ∈ zpowers a ↔ ∃! k : ℤ, a ^ k = b

Alias of Subgroup.mem_zpowers_iff_existsUnique_zpow.

---

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.

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

theorem AddSubgroup.mem_closure_singleton_iff_existsUnique_zsmul {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {a b : G} (ha : a ≠ 0) : b ∈ zmultiples a ↔ ∃! k : ℤ, k • a = b

Alias of AddSubgroup.mem_zmultiples_iff_existsUnique_zsmul.

---

The additive subgroup generated by an element of an additive group equals the set of integer multiples of the element, such that each multiple is a unique element. This is the stronger version of AddSubgroup.mem_closure_singleton.

theorem Int.addEquiv_eq_refl_or_neg (e : ℤ ≃+ ℤ) : e = AddEquiv.refl ℤ ∨ e = AddEquiv.neg ℤ

@[instance_reducible]

instance instFintypeAddEquivInt : Fintype (ℤ ≃+ ℤ)

Equations

• instFintypeAddEquivInt = { elems := Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_2, complete := ⋯ }

@[simp]

theorem Int.univ_addEquiv : Finset.univ = Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_2

@[simp]

theorem Int.card_fintype_addEquiv : Fintype.card (ℤ ≃+ ℤ) = 2

@[instance_reducible]

instance instUniqueOrderAddMonoidIsoInt : Unique (ℤ ≃+o ℤ)

Equations

• instUniqueOrderAddMonoidIsoInt = { toInhabited := OrderAddMonoidIso.instInhabited ℤ, uniq := instUniqueOrderAddMonoidIsoInt._proof_2 }

@[instance_reducible]

instance instUniqueOrderAddMonoidIsoIntOrderDual : Unique (ℤ ≃+o ℤᵒᵈ)

Equations

• One or more equations did not get rendered due to their size.

theorem Subgroup.isCyclic_of_disjoint_Ioo_one {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G} {a : G} (h₀ : 1 < a) (hd : Disjoint (↑H) (Set.Ioo 1 a)) : IsCyclic ↥H

If a subgroup of a linear ordered commutative group is disjoint with the interval Set.Ioo 1 a for some 1 < a, then this is a cyclic subgroup.

theorem AddSubgroup.isAddCyclic_of_disjoint_Ioo_zero {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {H : AddSubgroup G} {a : G} (h₀ : 0 < a) (hd : Disjoint (↑H) (Set.Ioo 0 a)) : IsAddCyclic ↥H

If an additive subgroup of a linear ordered additive commutative group is disjoint with the interval Set.Ioo 0 a for some positive a, then this is a cyclic subgroup.

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

theorem Subgroup.cyclic_of_isolated_one {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G} {a : G} (h₀ : 1 < a) (hd : Disjoint (↑H) (Set.Ioo 1 a)) : IsCyclic ↥H

Alias of Subgroup.isCyclic_of_disjoint_Ioo_one.

---

If a subgroup of a linear ordered commutative group is disjoint with the interval Set.Ioo 1 a for some 1 < a, then this is a cyclic subgroup.

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

theorem AddSubgroup.cyclic_of_isolated_zero {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {H : AddSubgroup G} {a : G} (h₀ : 0 < a) (hd : Disjoint (↑H) (Set.Ioo 0 a)) : IsAddCyclic ↥H

Alias of AddSubgroup.isAddCyclic_of_disjoint_Ioo_zero.

---

If an additive subgroup of a linear ordered additive commutative group is disjoint with the interval Set.Ioo 0 a for some positive a, then this is a cyclic subgroup.

noncomputable def LinearOrderedCommGroup.zpowersOrderMonoidIso {G : Type u_1} {G' : Type u_2} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [CommGroup G'] [LinearOrder G'] [IsOrderedMonoid G'] (x : G) (y : G') (hxy : x = 1 ↔ y = 1) : ↥(Subgroup.zpowers x) ≃*o ↥(Subgroup.zpowers y)

In two linearly ordered groups, the closure of an element of one group is isomorphic (and order-isomorphic) to the closure of an element in the other group.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LinearOrderedAddCommGroup.zmultiplesOrderAddMonoidIso {G : Type u_1} {G' : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [AddCommGroup G'] [LinearOrder G'] [IsOrderedAddMonoid G'] (x : G) (y : G') (hxy : x = 0 ↔ y = 0) : ↥(AddSubgroup.zmultiples x) ≃+o ↥(AddSubgroup.zmultiples y)

In two linearly ordered additive groups, the closure of an element of one group is isomorphic (and order-isomorphic) to the closure of an element in the other group.

Equations

• One or more equations did not get rendered due to their size.

@[deprecated LinearOrderedCommGroup.zpowersOrderMonoidIso (since := "2026-08-30")]

def LinearOrderedCommGroup.closure_equiv_closure {G : Type u_1} {G' : Type u_2} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [CommGroup G'] [LinearOrder G'] [IsOrderedMonoid G'] (x : G) (y : G') (hxy : x = 1 ↔ y = 1) : ↥(Subgroup.zpowers x) ≃*o ↥(Subgroup.zpowers y)

Alias of LinearOrderedCommGroup.zpowersOrderMonoidIso.

---

In two linearly ordered groups, the closure of an element of one group is isomorphic (and order-isomorphic) to the closure of an element in the other group.

Equations

• @LinearOrderedCommGroup.closure_equiv_closure = @LinearOrderedCommGroup.zpowersOrderMonoidIso

@[deprecated LinearOrderedAddCommGroup.zmultiplesOrderAddMonoidIso (since := "2026-08-30")]

noncomputable def LinearOrderedAddCommGroup.closure_equiv_closure {G : Type u_1} {G' : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [AddCommGroup G'] [LinearOrder G'] [IsOrderedAddMonoid G'] (x : G) (y : G') (hxy : x = 0 ↔ y = 0) : ↥(AddSubgroup.zmultiples x) ≃+o ↥(AddSubgroup.zmultiples y)

Alias of LinearOrderedAddCommGroup.zmultiplesOrderAddMonoidIso.

---

In two linearly ordered additive groups, the closure of an element of one group is isomorphic (and order-isomorphic) to the closure of an element in the other group.

Equations

• @LinearOrderedAddCommGroup.closure_equiv_closure = @LinearOrderedAddCommGroup.zmultiplesOrderAddMonoidIso

theorem Subgroup.isLeast_of_closure_iff_eq_mabs {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a b : G} : IsLeast {y : G | y ∈ zpowers a ∧ 1 < y} b ↔ b = |a|ₘ ∧ 1 < b

theorem AddSubgroup.isLeast_of_closure_iff_eq_abs {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {a b : G} : IsLeast {y : G | y ∈ zmultiples a ∧ 0 < y} b ↔ b = |a| ∧ 0 < b

noncomputable def LinearOrderedAddCommGroup.int_orderAddMonoidIso_of_isLeast_pos {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] {x : G} (h : IsLeast {y : G | 0 < y} x) : G ≃+o ℤ

If an element of a linearly ordered archimedean additive group is the least positive element, then the whole group is isomorphic (and order-isomorphic) to the integers.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LinearOrderedCommGroup.multiplicative_int_orderMonoidIso_of_isLeast_one_lt {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {x : G} (h : IsLeast {y : G | 1 < y} x) : G ≃*o Multiplicative ℤ

If an element of a linearly ordered mul-archimedean group is the least element greater than 1, then the whole group is isomorphic (and order-isomorphic) to the multiplicative integers.

Equations

• LinearOrderedCommGroup.multiplicative_int_orderMonoidIso_of_isLeast_one_lt h = OrderAddMonoidIso.toMultiplicativeRight (LinearOrderedAddCommGroup.int_orderAddMonoidIso_of_isLeast_pos h)

theorem Archimedean.of_locallyFiniteOrder {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [LocallyFiniteOrder G] : Archimedean G

Any locally finite linear additive group is archimedean.

theorem MulArchimedean.of_locallyFiniteOrder {G : Type u_2} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [LocallyFiniteOrder G] : MulArchimedean G

Any locally finite linear group is mul-archimedean.

theorem LinearOrderedAddCommGroup.discrete_or_denselyOrdered (G : Type u_2) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] : Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G

Any linearly ordered archimedean additive group is either isomorphic (and order-isomorphic) to the integers, or is densely ordered.

theorem LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered (G : Type u_2) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] : Nonempty (G ≃+o ℤ) ↔ ¬DenselyOrdered G

Any linearly ordered archimedean additive group is either isomorphic (and order-isomorphic) to the integers, or is densely ordered, exclusively.

(See also LinearOrderedAddCommGroup.isAddCyclic_iff_not_denselyOrdered.)

theorem LinearOrderedAddCommGroup.isAddCyclic_iff_not_denselyOrdered {A : Type u_2} [AddCommGroup A] [LinearOrder A] [IsOrderedAddMonoid A] [Archimedean A] [Nontrivial A] : IsAddCyclic A ↔ ¬DenselyOrdered A

Any non-trivial linearly ordered archimedean additive group is either cyclic, or densely ordered, exclusively.

theorem LinearOrderedCommGroup.discrete_or_denselyOrdered (G : Type u_1) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] : Nonempty (G ≃*o Multiplicative ℤ) ∨ DenselyOrdered G

Any linearly ordered mul-archimedean group is either isomorphic (and order-isomorphic) to the multiplicative integers, or is densely ordered.

theorem LinearOrderedCommGroup.discrete_iff_not_denselyOrdered (G : Type u_1) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] : Nonempty (G ≃*o Multiplicative ℤ) ↔ ¬DenselyOrdered G

Any linearly ordered mul-archimedean group is either isomorphic (and order-isomorphic) to the multiplicative integers, or is densely ordered, exclusively.

(See also LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered.)

theorem LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] [Nontrivial G] : IsCyclic G ↔ ¬DenselyOrdered G

Any non-trivial linearly ordered mul-archimedean group is either cyclic, or densely ordered, exclusively.

theorem LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered (G : Type u_2) [LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ] [MulArchimedean G] : Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ∨ DenselyOrdered G

Any nontrivial (has other than 0 and 1) linearly ordered mul-archimedean group with zero is either isomorphic (and order-isomorphic) to ℤᵐ⁰, or is densely ordered.

theorem LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered (G : Type u_2) [LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ] [MulArchimedean G] : Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ↔ ¬DenselyOrdered G

Any nontrivial (has other than 0 and 1) linearly ordered mul-archimedean group with zero is either isomorphic (and order-isomorphic) to ℤᵐ⁰, or is densely ordered, exclusively

theorem LinearOrderedAddCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Nontrivial G] {g : G} : ({x : G | g ≤ x}.WellFoundedOn fun (x1 x2 : G) => x1 < x2) ↔ Nonempty (G ≃+o ℤ)

@[deprecated LinearOrderedAddCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete (since := "2026-07-09")]

theorem LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Nontrivial G] {g : G} : ({x : G | g ≤ x}.WellFoundedOn fun (x1 x2 : G) => x1 < x2) ↔ Nonempty (G ≃+o ℤ)

Alias of LinearOrderedAddCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete.

theorem LinearOrderedAddCommGroup.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Nontrivial G] (g : G) : ({x : G | x ≤ g}.WellFoundedOn fun (x1 x2 : G) => x1 > x2) ↔ Nonempty (G ≃+o ℤ)

@[deprecated LinearOrderedAddCommGroup.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete (since := "2026-07-09")]

theorem LinearOrderedAddCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Nontrivial G] (g : G) : ({x : G | x ≤ g}.WellFoundedOn fun (x1 x2 : G) => x1 > x2) ↔ Nonempty (G ≃+o ℤ)

Alias of LinearOrderedAddCommGroup.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete.

theorem LinearOrderedCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete {G : Type u_2} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [Nontrivial G] {g : G} : ({x : G | g ≤ x}.WellFoundedOn fun (x1 x2 : G) => x1 < x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

@[deprecated LinearOrderedCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete (since := "2026-07-09")]

theorem LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete {G : Type u_2} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [Nontrivial G] {g : G} : ({x : G | g ≤ x}.WellFoundedOn fun (x1 x2 : G) => x1 < x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Alias of LinearOrderedCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete.

theorem LinearOrderedCommGroup.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete {G : Type u_2} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [Nontrivial G] (g : G) : ({x : G | x ≤ g}.WellFoundedOn fun (x1 x2 : G) => x1 > x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

@[deprecated LinearOrderedCommGroup.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete (since := "2026-07-09")]

theorem LinearOrderedCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete {G : Type u_2} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [Nontrivial G] (g : G) : ({x : G | x ≤ g}.WellFoundedOn fun (x1 x2 : G) => x1 > x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Alias of LinearOrderedCommGroup.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete.

theorem LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete_of_ne_zero {G₀ : Type u_2} [LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] {g : G₀} (hg : g ≠ 0) : ({x : G₀ | g ≤ x}.WellFoundedOn fun (x1 x2 : G₀) => x1 < x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))

@[deprecated LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete_of_ne_zero (since := "2026-07-09")]

theorem LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero {G₀ : Type u_2} [LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] {g : G₀} (hg : g ≠ 0) : ({x : G₀ | g ≤ x}.WellFoundedOn fun (x1 x2 : G₀) => x1 < x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))

Alias of LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete_of_ne_zero.

theorem LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete_of_ne_zero {G₀ : Type u_2} [LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] {g : G₀} (hg : g ≠ 0) : ({x : G₀ | x ≤ g}.WellFoundedOn fun (x1 x2 : G₀) => x1 > x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))

@[deprecated LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete_of_ne_zero (since := "2026-07-09")]

theorem LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero {G₀ : Type u_2} [LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] {g : G₀} (hg : g ≠ 0) : ({x : G₀ | x ≤ g}.WellFoundedOn fun (x1 x2 : G₀) => x1 > x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ))

Alias of LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete_of_ne_zero.

instance instWellFoundedGTWithZeroMultiplicativeIntLeOne : WellFoundedGT { v : WithZero (Multiplicative ℤ) // v ≤ 1 }

theorem OrderMonoidIso.mulArchimedean {α : Type u_2} {β : Type u_3} [CommMonoid α] [PartialOrder α] [CommMonoid β] [PartialOrder β] (e : α ≃*o β) [MulArchimedean α] : MulArchimedean β

theorem OrderAddMonoidIso.addArchimedean {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] (e : α ≃+o β) [Archimedean α] : Archimedean β

theorem WithZero.mulArchimedean_iff {α : Type u_2} [CommGroup α] [PartialOrder α] : MulArchimedean (WithZero α) ↔ MulArchimedean α

theorem Units.mulArchimedean_iff {G₀ : Type u_2} [LinearOrderedCommGroupWithZero G₀] : MulArchimedean G₀ˣ ↔ MulArchimedean G₀

@[instance_reducible]

instance instLocallyFiniteOrderMultiplicative {X : Type u_2} [Preorder X] [LocallyFiniteOrder X] : LocallyFiniteOrder (Multiplicative X)

Equations

• instLocallyFiniteOrderMultiplicative = OrderIso.locallyFiniteOrder { toEquiv := Multiplicative.toAdd, map_rel_iff' := ⋯ }

@[instance_reducible]

instance instLocallyFiniteOrderAdditive {X : Type u_2} [Preorder X] [LocallyFiniteOrder X] : LocallyFiniteOrder (Additive X)

Equations

• instLocallyFiniteOrderAdditive = OrderIso.locallyFiniteOrder { toEquiv := Additive.toMul, map_rel_iff' := ⋯ }

@[instance_reducible]

noncomputable instance instLocallyFiniteOrderUnits {X : Type u_2} [Preorder X] [LocallyFiniteOrder X] [Monoid X] : LocallyFiniteOrder Xˣ

Equations

• instLocallyFiniteOrderUnits = OrderEmbedding.locallyFiniteOrder { toFun := Units.val, inj' := ⋯, map_rel_iff' := ⋯ }

@[instance_reducible]

instance instLocallyFiniteOrderUnitsWithZero {X : Type u_2} [Preorder X] [LocallyFiniteOrder X] [Group X] : LocallyFiniteOrder (WithZero X)ˣ

Equations

• instLocallyFiniteOrderUnitsWithZero = (↑OrderMonoidIso.unitsWithZero).locallyFiniteOrder

theorem denselyOrdered_additive_iff {X : Type u_2} [LT X] : DenselyOrdered (Additive X) ↔ DenselyOrdered X

theorem denselyOrdered_multiplicative_iff {X : Type u_2} [LT X] : DenselyOrdered (Multiplicative X) ↔ DenselyOrdered X

instance instDenselyOrderedMultiplicative {X : Type u_2} [LT X] [DenselyOrdered X] : DenselyOrdered (Multiplicative X)

instance instDenselyOrderedAdditive {X : Type u_2} [LT X] [DenselyOrdered X] : DenselyOrdered (Additive X)

theorem WithZero.denselyOrdered_iff {M : Type u_3} [Preorder M] [NoMinOrder M] : DenselyOrdered (WithZero M) ↔ DenselyOrdered M

instance instDenselyOrderedWithZeroOfNoMinOrder {X : Type u_3} [Preorder X] [NoMinOrder X] [DenselyOrdered X] : DenselyOrdered (WithZero X)

theorem Int.not_denselyOrdered : ¬DenselyOrdered ℤ

theorem not_denselyOrdered_withZero_int : ¬DenselyOrdered (WithZero (Multiplicative ℤ))

theorem WithZero.denselyOrdered_set_iff_subsingleton {X : Type u_3} [LinearOrder X] [LocallyFiniteOrder X] {s : Set (WithZero X)} : DenselyOrdered ↑s ↔ s.Subsingleton