@[simp]

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

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

Equations

• ⋯ = ⋯