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 : } :
n1 = n2n1 = z1n2 = z2z1 = z2

theorem linarith.nat_le_subst {n1 n2 : } {z1 z2 : } :
n1 n2n1 = z1n2 = z2z1 z2

theorem linarith.nat_lt_subst {n1 n2 : } {z1 z2 : } :
n1 < n2n1 = z1n2 = z2z1 < z2

theorem linarith.eq_of_eq_of_eq {α : Type u_1} [ordered_semiring α] {a b : α} :
a = 0b = 0a + b = 0

theorem linarith.le_of_eq_of_le {α : Type u_1} [ordered_semiring α] {a b : α} :
a = 0b 0a + b 0

theorem linarith.lt_of_eq_of_lt {α : Type u_1} [ordered_semiring α] {a b : α} :
a = 0b < 0a + b < 0

theorem linarith.le_of_le_of_eq {α : Type u_1} [ordered_semiring α] {a b : α} :
a 0b = 0a + b 0

theorem linarith.lt_of_lt_of_eq {α : Type u_1} [ordered_semiring α] {a b : α} :
a < 0b = 0a + b < 0

theorem linarith.mul_neg {α : Type u_1} [ordered_ring α] {a b : α} :
a < 00 < bb * a < 0

theorem linarith.mul_nonpos {α : Type u_1} [ordered_ring α] {a b : α} :
a 00 < bb * a 0

@[nolint]
theorem linarith.mul_eq {α : Type u_1} [ordered_semiring α] {a b : α} :
a = 00 < bb * a = 0

theorem linarith.eq_of_not_lt_of_not_gt {α : Type u_1} [linear_order α] (a b : α) :
¬a < b¬b < aa = b

@[nolint]
theorem linarith.mul_zero_eq {α : Type u_1} {R : α → α → Prop} [semiring α] {a b : α} :
R a 0b = 0a * b = 0

@[nolint]
theorem linarith.zero_mul_eq {α : Type u_1} {R : α → α → Prop} [semiring α] {a b : α} :
a = 0R b 0a * b = 0