mathlib 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.

theorem linarith.int.coe_nat_bit0_mul (n x : ) :
(bit0 n * x) = (bit0 n) * x
theorem linarith.int.coe_nat_bit1_mul (n x : ) :
(bit1 n * x) = (bit1 n) * x
theorem linarith.int.coe_nat_one_mul (x : ) :
(1 * x) = 1 * x
theorem linarith.int.coe_nat_zero_mul (x : ) :
(0 * x) = 0 * x
theorem linarith.int.coe_nat_mul_bit0 (n x : ) :
(x * bit0 n) = x * (bit0 n)
theorem linarith.int.coe_nat_mul_bit1 (n x : ) :
(x * bit1 n) = x * (bit1 n)
theorem linarith.int.coe_nat_mul_one (x : ) :
(x * 1) = x * 1
theorem linarith.int.coe_nat_mul_zero (x : ) :
(x * 0) = x * 0
theorem linarith.nat_eq_subst {n1 n2 : } {z1 z2 : } (hn : n1 = n2) (h1 : n1 = z1) (h2 : n2 = z2) :
z1 = z2
theorem linarith.nat_le_subst {n1 n2 : } {z1 z2 : } (hn : n1 n2) (h1 : n1 = z1) (h2 : n2 = z2) :
z1 z2
theorem linarith.nat_lt_subst {n1 n2 : } {z1 z2 : } (hn : n1 < n2) (h1 : n1 = z1) (h2 : n2 = z2) :
z1 < z2
theorem linarith.eq_of_eq_of_eq {α : Type u_1} [ordered_semiring α] {a b : α} (ha : a = 0) (hb : b = 0) :
a + b = 0
theorem linarith.le_of_eq_of_le {α : Type u_1} [ordered_semiring α] {a b : α} (ha : a = 0) (hb : b 0) :
a + b 0
theorem linarith.lt_of_eq_of_lt {α : Type u_1} [ordered_semiring α] {a b : α} (ha : a = 0) (hb : b < 0) :
a + b < 0
theorem linarith.le_of_le_of_eq {α : Type u_1} [ordered_semiring α] {a b : α} (ha : a 0) (hb : b = 0) :
a + b 0
theorem linarith.lt_of_lt_of_eq {α : Type u_1} [ordered_semiring α] {a b : α} (ha : a < 0) (hb : b = 0) :
a + b < 0
theorem linarith.mul_neg {α : Type u_1} [ordered_ring α] {a b : α} (ha : a < 0) (hb : 0 < b) :
b * a < 0
theorem linarith.mul_nonpos {α : Type u_1} [ordered_ring α] {a b : α} (ha : a 0) (hb : 0 < b) :
b * a 0
@[nolint]
theorem linarith.mul_eq {α : Type u_1} [ordered_semiring α] {a b : α} (ha : a = 0) (hb : 0 < b) :
b * a = 0
theorem linarith.eq_of_not_lt_of_not_gt {α : Type u_1} [linear_order α] (a b : α) (h1 : ¬a < b) (h2 : ¬b < a) :
a = b
@[nolint]
theorem linarith.mul_zero_eq {α : Type u_1} {R : α → α → Prop} [semiring α] {a b : α} (_x : R a 0) (h : b = 0) :
a * b = 0
@[nolint]
theorem linarith.zero_mul_eq {α : Type u_1} {R : α → α → Prop} [semiring α] {a b : α} (h : a = 0) (_x : R b 0) :
a * b = 0