Theorems · Theorem · order theory
smul_add_smul_le_smul_add_smul
∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
[inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_7 : Module α β]
[PosSMulMono α β] {a₁ a₂ : α} {b₁ b₂ : β}, a₁ ≤ a₂ → b₁ ≤ b₂ → a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂Binary rearrangement inequality.
- Defined in
- Mathlib.Algebra.Order.Module.Defs
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- PartialOrderstatement and proof · cited by 6,410
- IsStrictOrderedRingstatement and proof · cited by 2,490
- le_reflproof · cited by 2,061
- add_le_addproof · cited by 666
- IsOrderedCancelAddMonoidstatement and proof · cited by 359
- ExistsAddOfLEstatement and proof · cited by 330
- add_smulproof · cited by 204
- PosSMulMonostatement and proof · cited by 188
- add_left_commproof · cited by 76
Cited by1
Results whose statement or proof uses this declaration.
- smul_add_smul_le_smul_add_smul'proof · cited by 1