Ordered groups have no top element

Stream: Is there code for X?

[Heather Macbeth]

Does this exist in some form? Also, is there a typeclass for not having a maximal element, the way that has_top is for having a maximal element?

import order.filter.at_top_bot
variables {β : Type*} [decidable_linear_ordered_add_comm_group β]

lemma exists_pos [nontrivial β] : ∃ b : β, 0 < b :=
begin
  obtain ⟨a, ha⟩ : ∃ a : β, a ≠ 0 := exists_ne 0,
  cases lt_or_gt_of_ne ha,
  { exact ⟨-a, neg_pos.mpr h⟩ },
  { exact ⟨a, h⟩ },
end

lemma not_has_top [nontrivial β] (c : β) : ∃ c', c < c' :=
begin
  obtain ⟨b, hb⟩ : ∃ b : β, 0 < b := exists_pos,
  exact ⟨c + b, lt_add_of_pos_right c hb⟩
end

[Reid Barton]

For the second question, docs#no_top_order

[Heather Macbeth]

Ah good. So to rephrase, it seems I'm asking about the existence of

instance foo [decidable_linear_ordered_add_comm_group β] [nontrivial β] : no_top_order β

[Heather Macbeth]

By looking to see how one gets no_top_order ℤ, I discovered linear_ordered_semiring.​to_no_top_order.

The instance I wrote would supersede linear_ordered_semiring.​to_no_top_order. Should I make this replacement? on second thoughts, I guess not all linear ordered semirings are decidable. If there were a preexisting typeclass linear_ordered_add_comm_group, that would be the right way to do a grand unified theory.

[Aaron Anderson]

This exists for linear_ordered_fields, and apparently separately for linear_ordered_(semi)ring

[Aaron Anderson]

Is there a reason not to have all the classes just be linear_ordered_thingy and then have a mixin for the order being decidable?

[Heather Macbeth]

I completely agree. I think there are a lot of similar issues in the order hierarchy, actually. For example, this.

[Heather Macbeth]

But that'd be a big refactor. Maybe for now I will just PR a documentation comment to linear_ordered_semiring and linear_ordered_field, so that when (someday) a typeclass linear_ordered_add_comm_group is created, the person doing it remembers to prove this theorem for it.