Monotonicity of the action by rational numbers

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[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

• ⋯ = ⋯