Monotonicity of the action by rational numbers

instance PosSMulMono.nnrat_of_rat {α : Type u_1} [Preorder α] [MulAction ℚ α] [MulAction ℚ≥0 α] [IsScalarTower ℚ≥0 ℚ α] [PosSMulMono ℚ α] : PosSMulMono ℚ≥0 α

instance PosSMulStrictMono.nnrat_of_rat {α : Type u_1} [Preorder α] [MulAction ℚ≥0 α] [MulAction ℚ α] [IsScalarTower ℚ≥0 ℚ α] [PosSMulStrictMono ℚ α] : PosSMulStrictMono ℚ≥0 α

@[simp]

theorem abs_nnqsmul {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [DistribMulAction ℚ≥0 α] [PosSMulMono ℚ≥0 α] (q : ℚ≥0) (a : α) : |q • a| = q • |a|

@[deprecated abs_smul (since := "2025-06-24")]

theorem abs_qsmul {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Module ℚ α] [PosSMulMono ℚ α] (q : ℚ) (a : α) : |q • a| = |q| • |a|

instance LinearOrderedSemifield.toPosSMulStrictMono_rat {α : Type u_1} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] : PosSMulStrictMono ℚ≥0 α

instance LinearOrderedField.toPosSMulStrictMono_rat {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] : PosSMulStrictMono ℚ α