# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Ordered groups have no top element

#### Heather Macbeth (Aug 14 2020 at 18:26):

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 (Aug 14 2020 at 18:30):

For the second question, docs#no_top_order

#### Heather Macbeth (Aug 14 2020 at 18:37):

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 (Aug 14 2020 at 19:01):

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 ~~ on second thoughts, I guess not all linear ordered semirings are decidable. If there were a preexisting typeclass `linear_ordered_semiring.to_no_top_order`

. Should I make this replacement?`linear_ordered_add_comm_group`

, that would be the right way to do a grand unified theory.

#### Aaron Anderson (Aug 14 2020 at 19:58):

This exists for `linear_ordered_field`

s, and apparently separately for `linear_ordered_(semi)ring`

#### Aaron Anderson (Aug 14 2020 at 20:01):

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 (Aug 14 2020 at 20:13):

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

#### Heather Macbeth (Aug 14 2020 at 20:15):

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.

Last updated: May 16 2021 at 05:21 UTC