Documentation

Mathlib.Data.Int.Order.Basic

The order relation on the integers #

theorem Int.le.elim {a : } {b : } (h : a b) {P : Prop} (h' : ∀ (n : ), a + n = bP) :
P
theorem Int.le_of_ofNat_le_ofNat {m : } {n : } :
m nm n

Alias of the forward direction of Int.ofNat_le.

theorem Int.ofNat_le_ofNat_of_le {m : } {n : } :
m nm n

Alias of the reverse direction of Int.ofNat_le.

theorem Int.lt.elim {a : } {b : } (h : a < b) {P : Prop} (h' : ∀ (n : ), a + n.succ = bP) :
P
theorem Int.lt_of_ofNat_lt_ofNat {n : } {m : } :
n < mn < m

Alias of the forward direction of Int.ofNat_lt.

theorem Int.ofNat_lt_ofNat_of_lt {n : } {m : } :
n < mn < m

Alias of the reverse direction of Int.ofNat_lt.

@[deprecated Int.mul_neg]
theorem Int.mul_neg_eq_neg_mul_symm (a : ) (b : ) :
a * -b = -(a * b)

Alias of Int.mul_neg.

@[deprecated Int.neg_mul]
theorem Int.neg_mul_eq_neg_mul_symm (a : ) (b : ) :
-a * b = -(a * b)

Alias of Int.neg_mul.

theorem Int.eq_zero_or_eq_zero_of_mul_eq_zero {a : } {b : } (h : a * b = 0) :
a = 0 b = 0
theorem Int.nonneg_or_nonpos_of_mul_nonneg {a : } {b : } :
0 a * b0 a 0 b a 0 b 0
theorem Int.mul_nonneg_of_nonneg_or_nonpos {a : } {b : } :
0 a 0 b a 0 b 00 a * b
theorem Int.mul_nonneg_iff {a : } {b : } :
0 a * b 0 a 0 b a 0 b 0