Mathlib Map

Theorems · Theorem · order theory

add_le_mul_of_left_le_right

∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [ZeroLEOneClass R] [NeZero 1] [MulPosStrictMono R]
  [AddLeftMono R], 2 ≤ a → a ≤ b → a + b ≤ a * b
Defined in
Mathlib.Algebra.Order.Ring.Unbundled.Basic
Cited by
1 results in Mathlib
Foundations
Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SemiringLinearOrderZeroLEOneClassNeZeroMulPosStrictMonoAddLeftMono
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

add_le_mul · cited by 2add_le_mulSemiring · cited by 13802SemiringLinearOrder · cited by 8572LinearOrderle_refl · cited by 2061le_reflAddLeftMono · cited by 687AddLeftMonoadd_le_add · cited by 666add_le_addZeroLEOneClass · cited by 304ZeroLEOneClasstwo_mul · cited by 232two_mulzero_lt_two · cited by 124zero_lt_twoMulPosStrictMono · cited by 94MulPosStrictMonomul_le_mul_iff_left₀ · cited by 19mul_le_mul_iff_left₀add_le_mul_of_left_le_rightCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.