Documentation

Mathlib.Algebra.Order.Module.Rat

Monotonicity of the action by rational numbers #

@[simp]
theorem abs_qsmul {α : Type u_1} [LinearOrderedAddCommGroup α] [Module α] [PosSMulMono α] (q : ) (a : α) :