Theorems · Theorem · order theory
smul_mono_right
∀ {M : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : Preorder α] [CovariantClass M α HSMul.hSMul LE.le] (m : M),
Monotone (HSMul.hSMul m)- Defined in
- Mathlib.Algebra.Order.Group.Action
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- SMulPreorderCovariantClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- Monotonestatement · cited by 1,397
- CovariantClassstatement and proof · cited by 25
- CovariantClass.elimproof · cited by 22
Cited by18
Results whose statement or proof uses this declaration.
- smul_le_smul_leftproof · cited by 5
- Ideal.mul_mono_rightproof · cited by 5
- Ideal.pointwise_smul_le_pointwise_smul_iffproof · cited by 2
- lipschitzGroup.conjAct_smul_range_ιproof · cited by 2
- Submodule.smul_top_le_comap_smul_topproof · cited by 2
- Ideal.Filtration.Stable.exists_forall_leproof · cited by 1
- smul_eq_of_le_smulproof · cited by 1
- AdicCompletion.map_injectiveproof · cited by 1
- pow_smul_leproof · cited by 1
- Ideal.Filtration.pow_smul_leproof · cited by 1
- Ideal.Filtration.pow_smul_le_pow_smulproof · cited by 1
- le_pow_smulproof · cited by 1