feat(ring_theory/subring): weaken typeclass assumption for `units.pos…

…_subgroup` (#10332)





Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/ring_theory/subring.lean

@@ -1000,11 +1000,11 @@ end actions
 -- both ordered ring structures and submonoids available
 
 /-- The subgroup of positive units of a linear ordered commutative ring. -/
-def units.pos_subgroup (R : Type*) [linear_ordered_comm_ring R] [nontrivial R] :
+def units.pos_subgroup (R : Type*) [linear_ordered_semiring 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 R).comap (units.coe_hom R)}
 
-@[simp] lemma units.mem_pos_subgroup {R : Type*} [linear_ordered_comm_ring R] [nontrivial R]
+@[simp] lemma units.mem_pos_subgroup {R : Type*} [linear_ordered_semiring R]
   (u : units R) : u ∈ units.pos_subgroup R ↔ (0 : R) < u := iff.rfl