mathlib3 documentation

tactic.linarith.lemmas

Lemmas for linarith #

This file contains auxiliary lemmas that linarith uses to construct proofs. If you find yourself looking for a theorem here, you might be in the wrong place.

source
theorem linarith.zero_lt_one {α : Type u_1} [ordered_semiring α] [nontrivial α] :
0 < 1
source
theorem linarith.eq_of_eq_of_eq {α : Type u_1} [ordered_semiring α] {a b : α} (ha : a = 0) (hb : b = 0) :
a + b = 0
source
theorem linarith.le_of_eq_of_le {α : Type u_1} [ordered_semiring α] {a b : α} (ha : a = 0) (hb : b ≤ 0) :
a + b ≤ 0
source
theorem linarith.lt_of_eq_of_lt {α : Type u_1} [ordered_semiring α] {a b : α} (ha : a = 0) (hb : b < 0) :
a + b < 0
source
theorem linarith.le_of_le_of_eq {α : Type u_1} [ordered_semiring α] {a b : α} (ha : a ≤ 0) (hb : b = 0) :
a + b ≤ 0
source
theorem linarith.lt_of_lt_of_eq {α : Type u_1} [ordered_semiring α] {a b : α} (ha : a < 0) (hb : b = 0) :
a + b < 0
source
theorem linarith.mul_neg {α : Type u_1} [strict_ordered_ring α] {a b : α} (ha : a < 0) (hb : 0 < b) :
b * a < 0
source
theorem linarith.mul_nonpos {α : Type u_1} [ordered_ring α] {a b : α} (ha : a ≤ 0) (hb : 0 < b) :
b * a ≤ 0
source
@[nolint]
theorem linarith.mul_eq {α : Type u_1} [ordered_semiring α] {a b : α} (ha : a = 0) (hb : 0 < b) :
b * a = 0
source
theorem linarith.eq_of_not_lt_of_not_gt {α : Type u_1} [linear_order α] (a b : α) (h1 : ¬a < b) (h2 : ¬b < a) :
a = b
source
@[nolint]
theorem linarith.mul_zero_eq {α : Type u_1} {R : α → α → Prop} [semiring α] {a b : α} (_x : R a 0) (h : b = 0) :
a * b = 0
source
@[nolint]
theorem linarith.zero_mul_eq {α : Type u_1} {R : α → α → Prop} [semiring α] {a b : α} (h : a = 0) (_x : R b 0) :
a * b = 0