feat: Submonoid of nonnegative elements (#10209)

Define the `Submonoid` of elements greater than `1`, the `AddSubmonoid` of nonnegative elements, move `posSubmonoid` with them and rename it to `Submonoid.pos`.

From LeanAPAP and partly extracted from #4871

Mathlib/GroupTheory/Submonoid/Operations.lean

@@ -5,6 +5,8 @@ Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzza
 Amelia Livingston, Yury Kudryashov
 -/
 import Mathlib.Algebra.Order.Monoid.Basic
+import Mathlib.Algebra.Order.Ring.Lemmas
+import Mathlib.Algebra.Order.ZeroLEOne
 import Mathlib.GroupTheory.GroupAction.Defs
 import Mathlib.GroupTheory.Submonoid.Basic
 import Mathlib.GroupTheory.Subsemigroup.Operations
@@ -1559,3 +1561,39 @@ instance mulDistribMulAction [Monoid α] [MulDistribMulAction M' α] (S : Submon
   MulDistribMulAction.compHom _ S.subtype
 
 example {S : Submonoid M'} : IsScalarTower S M' M' := by infer_instance
+
+section Preorder
+variable (M)
+variable [Preorder M] [CovariantClass M M (· * ·) (· ≤ ·)] {a : M}
+
+/-- The submonoid of elements greater than `1`. -/
+@[to_additive (attr := simps) nonneg "The submonoid of nonnegative elements."]
+def oneLE : Submonoid M where
+  carrier := Set.Ici 1
+  mul_mem' := one_le_mul
+  one_mem' := le_rfl
+
+variable {M}
+
+@[to_additive (attr := simp)] lemma mem_oneLE : a ∈ oneLE M ↔ 1 ≤ a := Iff.rfl
+
+end Preorder
+
+section MulZeroClass
+variable (α) [MulZeroOneClass α] [PartialOrder α] [PosMulStrictMono α] [ZeroLEOneClass α]
+  [NeZero (1 : α)] {a : α}
+
+/-- The submonoid of positive elements. -/
+@[simps] def pos : Submonoid α where
+  carrier := Set.Ioi 0
+  one_mem' := zero_lt_one
+  mul_mem' := mul_pos
+#align pos_submonoid Submonoid.pos
+
+variable {α}
+
+@[simp] lemma mem_pos : a ∈ pos α ↔ 0 < a := Iff.rfl
+#align mem_pos_monoid Submonoid.mem_pos
+
+end MulZeroClass
+end Submonoid

Mathlib/RingTheory/Subring/Basic.lean

@@ -1534,7 +1534,7 @@ end Actions
 -- both ordered ring structures and submonoids available
 /-- The subgroup of positive units of a linear ordered semiring. -/
 def Units.posSubgroup (R : Type*) [LinearOrderedSemiring R] : Subgroup Rˣ :=
-  { (posSubmonoid R).comap (Units.coeHom R) with
+  { (Submonoid.pos R).comap (Units.coeHom R) with
     carrier := { x | (0 : R) < x }
     inv_mem' := Units.inv_pos.mpr }
 #align units.pos_subgroup Units.posSubgroup

Mathlib/RingTheory/Subsemiring/Basic.lean

@@ -1470,18 +1470,11 @@ end Subsemiring
 
 end Actions
 
--- While this definition is not about `Subsemiring`s, this is the earliest we have
--- both `StrictOrderedSemiring` and `Submonoid` available.
-/-- Submonoid of positive elements of an ordered semiring. -/
-def posSubmonoid (R : Type*) [StrictOrderedSemiring R] : Submonoid R
-    where
-  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
-#align pos_submonoid posSubmonoid
-
-@[simp]
-theorem mem_posSubmonoid {R : Type*} [StrictOrderedSemiring R] (u : Rˣ) :
-    ↑u ∈ posSubmonoid R ↔ (0 : R) < u :=
-  Iff.rfl
-#align mem_pos_monoid mem_posSubmonoid
+/-- The set of nonnegative elements in an ordered semiring, as a subsemiring. -/
+@[simps]
+def Subsemiring.nonneg (R : Type*) [OrderedSemiring R] : Subsemiring R where
+  carrier := Set.Ici 0
+  mul_mem' := mul_nonneg
+  one_mem' := zero_le_one
+  add_mem' := add_nonneg
+  zero_mem' := le_rfl