Documentation

Mathlib.Algebra.Order.Module.Rat

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|