Theorems · Theorem · order theory
smul_add_smul_lt_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 α β]
[PosSMulStrictMono α β] {a₁ a₂ : α} {b₁ b₂ : β}, a₁ < a₂ → b₁ < b₂ → a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂Binary strict rearrangement inequality.
- Defined in
- Mathlib.Algebra.Order.Module.Defs
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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
- IsOrderedCancelAddMonoidstatement and proof · cited by 359
- ExistsAddOfLEstatement and proof · cited by 330
- add_smulproof · cited by 204
- PosSMulStrictMonostatement and proof · cited by 128
- add_left_commproof · cited by 76
- add_lt_add_rightproof · cited by 50
- smul_lt_smul_of_pos_leftproof · cited by 23
Cited by2
Results whose statement or proof uses this declaration.
- MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iffproof · cited by 5
- smul_add_smul_lt_smul_add_smul'proof · cited by 0