The order relation on the integers

theorem Int.le.elim {a : ℤ} {b : ℤ} (h : a ≤ b) {P : Prop} (h' : ∀ (n : ℕ), a + ↑n = b → P) : P

theorem Int.le_of_ofNat_le_ofNat {m : ℕ} {n : ℕ} : ↑m ≤ ↑n → m ≤ n

Alias of the forward direction of Int.ofNat_le.

theorem Int.ofNat_le_ofNat_of_le {m : ℕ} {n : ℕ} : m ≤ n → ↑m ≤ ↑n

Alias of the reverse direction of Int.ofNat_le.

theorem Int.lt.elim {a : ℤ} {b : ℤ} (h : a < b) {P : Prop} (h' : ∀ (n : ℕ), a + ↑(Nat.succ n) = b → P) : P

theorem Int.ofNat_lt_ofNat_of_lt {n : ℕ} {m : ℕ} : n < m → ↑n < ↑m

Alias of the reverse direction of Int.ofNat_lt.

theorem Int.lt_of_ofNat_lt_ofNat {n : ℕ} {m : ℕ} : ↑n < ↑m → n < m

Alias of the forward direction of Int.ofNat_lt.

instance Int.instLinearOrderInt : LinearOrder ℤ

Equations

• Int.instLinearOrderInt = LinearOrder.mk Int.le_total inferInstance inferInstance inferInstance

theorem Int.neg_mul_eq_neg_mul_symm (a : ℤ) (b : ℤ) : -a * b = -(a * b)

theorem Int.mul_neg_eq_neg_mul_symm (a : ℤ) (b : ℤ) : a * -b = -(a * b)

theorem Int.eq_zero_or_eq_zero_of_mul_eq_zero {a : ℤ} {b : ℤ} (h : a * b = 0) : a = 0 ∨ b = 0