feat: PosSMulMono ℚ α → PosSMulMono ℚ≥0 α (#17217)

From LeanAPAP
leanprover-community · Oct 17, 2024 · 090e243 · 090e243
1 parent 8306205
commit 090e243
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/Mathlib/Algebra/Order/Module/Rat.lean b/Mathlib/Algebra/Order/Module/Rat.lean
@@ -12,6 +12,12 @@ import Mathlib.Data.Rat.Cast.Order
 
 variable {α : Type*}
 
+instance PosSMulMono.nnrat_of_rat [Preorder α] [MulAction ℚ α] [PosSMulMono ℚ α] :
+    PosSMulMono ℚ≥0 α where elim _q hq _a₁ _a₂ ha := smul_le_smul_of_nonneg_left (α := ℚ) ha hq
+
+instance PosSMulStrictMono.nnrat_of_rat [Preorder α] [MulAction ℚ α] [PosSMulStrictMono ℚ α] :
+    PosSMulStrictMono ℚ≥0 α where elim _q hq _a₁ _a₂ ha := smul_lt_smul_of_pos_left (α := ℚ) ha hq
+
 section LinearOrderedAddCommGroup
 variable [LinearOrderedAddCommGroup α]