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 : ℤ} :

n1 = n2 → ↑n1 = z1 → ↑n2 = z2 → z1 = z2

source

theorem linarith.nat_le_subst {n1 n2 : ℕ} {z1 z2 : ℤ} :

n1 ≤ n2 → ↑n1 = z1 → ↑n2 = z2 → z1 ≤ z2

source

theorem linarith.nat_lt_subst {n1 n2 : ℕ} {z1 z2 : ℤ} :

n1 < n2 → ↑n1 = z1 → ↑n2 = z2 → z1 < z2

source

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

a = 0 → b = 0 → a + b = 0

source

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

a = 0 → b ≤ 0 → a + b ≤ 0

source

theorem linarith.lt_of_eq_of_lt {α : Type u_1} [ordered_semiring α] {a b : α} :

a = 0 → b < 0 → a + b < 0

source

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

a ≤ 0 → b = 0 → a + b ≤ 0

source

theorem linarith.lt_of_lt_of_eq {α : Type u_1} [ordered_semiring α] {a b : α} :

a < 0 → b = 0 → a + b < 0

source

theorem linarith.mul_neg {α : Type u_1} [ordered_ring α] {a b : α} :

a < 0 → 0 < b → b * a < 0

source

theorem linarith.mul_nonpos {α : Type u_1} [ordered_ring α] {a b : α} :

a ≤ 0 → 0 < b → b * a ≤ 0

source

@[nolint]

theorem linarith.mul_eq {α : Type u_1} [ordered_semiring α] {a b : α} :

a = 0 → 0 < b → b * a = 0

source

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

¬a < b → ¬b < a → a = b

source

@[nolint]

theorem linarith.mul_zero_eq {α : Type u_1} {R : α → α → Prop} [semiring α] {a b : α} :

R a 0 → b = 0 → a * b = 0

source

@[nolint]

theorem linarith.zero_mul_eq {α : Type u_1} {R : α → α → Prop} [semiring α] {a b : α} :

a = 0 → R b 0 → a * b = 0

mathlib documentation

tactic.linarith.lemmas

Lemmas for `linarith`

General documentation

Additional documentation

Library

mathlib documentation

tactic.​linarith.​lemmas

Lemmas for linarith

General documentation

Additional documentation

Library

tactic.linarith.lemmas

Lemmas for `linarith`