The submonoid of positive elements

Stream: Is there code for X?

[Eric Wieser]

Do either of these exist?

import algebra.ordered_ring
import ring_theory.subsemiring
import group_theory.subgroup

def pos_submonoid {R : Type*} [ordered_semiring R] [nontrivial R] : submonoid R :=
{ carrier := {x | 0 < x},
  one_mem' := show (0 : R) < 1, from zero_lt_one,
  mul_mem' := λ x y (hx : 0 < x) (hy : 0 < y), mul_pos hx hy }

def units.pos_subgroup {R : Type*} [linear_ordered_comm_ring R] [nontrivial R] : subgroup (units R) :=
{ carrier := {x | (0 : R) < x},
  inv_mem' := λ x (hx : (0 : R) < x), (zero_lt_mul_left hx).mp $ x.mul_inv.symm ▸ zero_lt_one,
  ..pos_submonoid.comap (units.coe_hom R)}

[Eric Wieser]

And if these don't exist, which file should they live in?

[Damiano Testa]

I was going to add something similar to work with orders on semirings where you want multiplication by positive elements to be monotone. However, I got slowed down in the process and did not get around yet to PRing this. Feel free to do so yourself!

[Eric Wieser]

Do you have a feel for where this could live?

[Damiano Testa]

My idea was to put this in a new file.

My application would be to use it in algebra.ordered_ring and later files. If you do not like a new file, then maybe some file imported by ordered_ring? I'm not at a computer this weekend, so I am not really able to find a home efficiently.