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.

source
theorem linarith.int.coe_nat_bit0 (n : ℕ) :
↑(bit0 n) = bit0 ↑n
source
theorem linarith.int.coe_nat_bit1 (n : ℕ) :
↑(bit1 n) = bit1 ↑n
source
theorem linarith.int.coe_nat_bit0_mul (n x : ℕ) :
↑(bit0 n * x) = ↑(bit0 n) * ↑x
source
theorem linarith.int.coe_nat_bit1_mul (n x : ℕ) :
↑(bit1 n * x) = ↑(bit1 n) * ↑x
source
theorem linarith.int.coe_nat_one_mul (x : ℕ) :
↑(1 * x) = 1 * ↑x
source
theorem linarith.int.coe_nat_zero_mul (x : ℕ) :
↑(0 * x) = 0 * ↑x
source
theorem linarith.int.coe_nat_mul_bit0 (n x : ℕ) :
↑(x * bit0 n) = ↑x * ↑(bit0 n)
source
theorem linarith.int.coe_nat_mul_bit1 (n x : ℕ) :
↑(x * bit1 n) = ↑x * ↑(bit1 n)
source
theorem linarith.int.coe_nat_mul_one (x : ℕ) :
↑(x * 1) = ↑x * 1
source
theorem linarith.int.coe_nat_mul_zero (x : ℕ) :
↑(x * 0) = ↑x * 0
source
theorem linarith.nat_eq_subst {n1 n2 : ℕ} {z1 z2 : ℤ} (hn : n1 = n2) (h1 : ↑n1 = z1) (h2 : ↑n2 = z2) :
z1 = z2
source
theorem linarith.nat_le_subst {n1 n2 : ℕ} {z1 z2 : ℤ} (hn : n1 ≤ n2) (h1 : ↑n1 = z1) (h2 : ↑n2 = z2) :
z1 ≤ z2
source
theorem linarith.nat_lt_subst {n1 n2 : ℕ} {z1 z2 : ℤ} (hn : n1 < n2) (h1 : ↑n1 = z1) (h2 : ↑n2 = z2) :
z1 < z2
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} [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