Theorems · Theorem · order theory

smul_le_smul_left

∀ {M : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : Preorder α] [CovariantClass M α HSMul.hSMul LE.le] (m : M)
  {a b : α}, a ≤ b → m • a ≤ m • b

A copy of smul_mono_right that is understood by gcongr.

Defined in

Mathlib.Algebra.Order.Group.Action

Cited by

5 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

SMulPreorderCovariantClass