Lemmas for linarith
. #
Those in the Linarith
namespace should stay here.
Those outside the Linarith
namespace may be deleted as they are ported to mathlib4.
theorem
Linarith.eq_of_eq_of_eq
{α : Type u_1}
[OrderedSemiring α]
{a b : α}
(ha : a = 0)
(hb : b = 0)
:
theorem
Linarith.le_of_eq_of_le
{α : Type u_1}
[OrderedSemiring α]
{a b : α}
(ha : a = 0)
(hb : b ≤ 0)
:
theorem
Linarith.lt_of_eq_of_lt
{α : Type u_1}
[OrderedSemiring α]
{a b : α}
(ha : a = 0)
(hb : b < 0)
:
theorem
Linarith.le_of_le_of_eq
{α : Type u_1}
[OrderedSemiring α]
{a b : α}
(ha : a ≤ 0)
(hb : b = 0)
:
theorem
Linarith.lt_of_lt_of_eq
{α : Type u_1}
[OrderedSemiring α]
{a b : α}
(ha : a < 0)
(hb : b = 0)
:
Finds the name of a multiplicative lemma corresponding to an inequality strength.
Equations
- Mathlib.Ineq.lt.toConstMulName = `Linarith.mul_neg
- Mathlib.Ineq.le.toConstMulName = `Linarith.mul_nonpos
- Mathlib.Ineq.eq.toConstMulName = `Linarith.mul_eq
Instances For
theorem
Linarith.eq_of_not_lt_of_not_gt
{α : Type u_1}
[LinearOrder α]
(a b : α)
(h1 : ¬a < b)
(h2 : ¬b < a)
:
a = b
@[deprecated Linarith.natCast_nonneg]
Alias of Linarith.natCast_nonneg
.