Monotonicity of the action by rational numbers #
instance
PosSMulStrictMono.nnrat_of_rat
{α : Type u_1}
[Preorder α]
[MulAction ℚ α]
[PosSMulStrictMono ℚ α]
:
@[simp]
theorem
abs_nnqsmul
{α : Type u_1}
[LinearOrderedAddCommGroup α]
[DistribMulAction ℚ≥0 α]
[PosSMulMono ℚ≥0 α]
(q : ℚ≥0)
(a : α)
: