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