Monotonicity of the action by rational numbers

@[simp]

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯