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 + ↑n.succ = b → P) : P

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

Alias of the forward direction of Int.ofNat_lt.

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

Alias of the reverse direction of Int.ofNat_lt.

@[implicit_reducible]

instance Int.instLinearOrder : LinearOrder ℤ

Equations

• One or more equations did not get rendered due to their size.

theorem Int.eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} : a * b = 0 → a = 0 ∨ b = 0

Alias of the forward direction of Int.mul_eq_zero.

theorem Int.nonneg_or_nonpos_of_mul_nonneg {a b : ℤ} : 0 ≤ a * b → 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem Int.mul_nonneg_of_nonneg_or_nonpos {a b : ℤ} : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 → 0 ≤ a * b

theorem Int.mul_nonneg_iff {a b : ℤ} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem Int.mul_pos_iff {a b : ℤ} : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

theorem Int.mul_nonpos_iff {a b : ℤ} : a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

theorem Int.mul_neg_iff {a b : ℤ} : a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b