mathlib3 documentation

core / init.data.int.order

source
@[irreducible]
def int.nonneg (a : ℤ) :
Prop
Equations
source
@[protected]
def int.le (a b : ℤ) :
Prop
Equations
source
@[protected, instance]
def int.has_le  :
has_le ℤ
Equations
source
@[protected]
def int.lt (a b : ℤ) :
Prop
Equations
source
@[protected, instance]
def int.has_lt  :
has_lt ℤ
Equations
source
def int.decidable_nonneg (a : ℤ) :
decidable a.nonneg
Equations
source
@[protected, instance]
def int.decidable_le (a b : ℤ) :
decidable (a ≤ b)
Equations
source
@[protected, instance]
def int.decidable_lt (a b : ℤ) :
decidable (a < b)
Equations
source
theorem int.lt_iff_add_one_le (a b : ℤ) :
a < b ↔ a + 1 ≤ b
source
theorem int.nonneg.elim {a : ℤ} :
a.nonneg → (∃ (n : ℕ), a = ↑n)
source
theorem int.nonneg_or_nonneg_neg (a : ℤ) :
a.nonneg ∨ (-a).nonneg
source
theorem int.le.intro_sub {a b : ℤ} {n : ℕ} (h : b - a = ↑n) :
a ≤ b
source
theorem int.le.intro {a b : ℤ} {n : ℕ} (h : a + ↑n = b) :
a ≤ b
source
theorem int.le.dest_sub {a b : ℤ} (h : a ≤ b) :
∃ (n : ℕ), b - a = ↑n
source
theorem int.le.dest {a b : ℤ} (h : a ≤ b) :
∃ (n : ℕ), a + ↑n = b
source
theorem int.le.elim {a b : ℤ} (h : a ≤ b) {P : Prop} (h' : ∀ (n : ℕ), a + ↑n = b → P) :
P
source
@[protected]
theorem int.le_total (a b : ℤ) :
a ≤ b ∨ b ≤ a
source
theorem int.coe_nat_le_coe_nat_of_le {m n : ℕ} (h : m ≤ n) :
↑m ≤ ↑n
source
theorem int.le_of_coe_nat_le_coe_nat {m n : ℕ} (h : ↑m ≤ ↑n) :
m ≤ n
source
theorem int.coe_nat_le_coe_nat_iff (m n : ℕ) :
↑m ≤ ↑n ↔ m ≤ n
source
theorem int.coe_zero_le (n : ℕ) :
0 ≤ ↑n
source
theorem int.eq_coe_of_zero_le {a : ℤ} (h : 0 ≤ a) :
∃ (n : ℕ), a = ↑n
source
theorem int.eq_succ_of_zero_lt {a : ℤ} (h : 0 < a) :
∃ (n : ℕ), a = ↑(n.succ)
source
theorem int.lt_add_succ (a : ℤ) (n : ℕ) :
a < a + ↑(n.succ)
source
theorem int.lt.intro {a b : ℤ} {n : ℕ} (h : a + ↑(n.succ) = b) :
a < b
source
theorem int.lt.dest {a b : ℤ} (h : a < b) :
∃ (n : ℕ), a + ↑(n.succ) = b
source
theorem int.lt.elim {a b : ℤ} (h : a < b) {P : Prop} (h' : ∀ (n : ℕ), a + ↑(n.succ) = b → P) :
P
source
theorem int.coe_nat_lt_coe_nat_iff (n m : ℕ) :
↑n < ↑m ↔ n < m
source
theorem int.lt_of_coe_nat_lt_coe_nat {m n : ℕ} (h : ↑m < ↑n) :
m < n
source
theorem int.coe_nat_lt_coe_nat_of_lt {m n : ℕ} (h : m < n) :
↑m < ↑n

show that the integers form an ordered additive group

source
@[protected]
theorem int.le_refl (a : ℤ) :
a ≤ a
source
@[protected]
theorem int.le_trans {a b c : ℤ} (h₁ : a ≤ b) (h₂ : b ≤ c) :
a ≤ c
source
@[protected]
theorem int.le_antisymm {a b : ℤ} (h₁ : a ≤ b) (h₂ : b ≤ a) :
a = b
source
@[protected]
theorem int.lt_irrefl (a : ℤ) :
¬a < a
source
@[protected]
theorem int.ne_of_lt {a b : ℤ} (h : a < b) :
a ≠ b
source
theorem int.le_of_lt {a b : ℤ} (h : a < b) :
a ≤ b
source
@[protected]
theorem int.lt_iff_le_and_ne (a b : ℤ) :
a < b ↔ a ≤ b ∧ a ≠ b
source
theorem int.lt_succ (a : ℤ) :
a < a + 1
source
@[protected]
theorem int.add_le_add_left {a b : ℤ} (h : a ≤ b) (c : ℤ) :
c + a ≤ c + b
source
@[protected]
theorem int.add_lt_add_left {a b : ℤ} (h : a < b) (c : ℤ) :
c + a < c + b
source
@[protected]
theorem int.mul_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) :
0 ≤ a * b
source
@[protected]
theorem int.mul_pos {a b : ℤ} (ha : 0 < a) (hb : 0 < b) :
0 < a * b
source
@[protected]
theorem int.zero_lt_one  :
0 < 1
source
@[protected]
theorem int.lt_iff_le_not_le {a b : ℤ} :
a < b ↔ a ≤ b ∧ ¬b ≤ a
source
@[protected, instance]
def int.linear_order  :
linear_order ℤ
Equations
source
theorem int.eq_nat_abs_of_zero_le {a : ℤ} (h : 0 ≤ a) :
a = ↑(a.nat_abs)
source
theorem int.le_nat_abs {a : ℤ} :
a ≤ ↑(a.nat_abs)
source
theorem int.neg_succ_lt_zero (n : ℕ) :
-[1+ n] < 0
source
theorem int.eq_neg_succ_of_lt_zero {a : ℤ} :
a < 0 → (∃ (n : ℕ), a = -[1+ n])

int is an ordered add comm group

source
@[protected]
theorem int.eq_neg_of_eq_neg {a b : ℤ} (h : a = -b) :
b = -a
source
@[protected]
theorem int.neg_add_cancel_left (a b : ℤ) :
-a + (a + b) = b
source
@[protected]
theorem int.add_neg_cancel_left (a b : ℤ) :
a + (-a + b) = b
source
@[protected]
theorem int.add_neg_cancel_right (a b : ℤ) :
a + b + -b = a
source
@[protected]
theorem int.neg_add_cancel_right (a b : ℤ) :
a + -b + b = a
source
@[protected]
theorem int.sub_self (a : ℤ) :
a - a = 0
source
@[protected]
theorem int.sub_eq_zero_of_eq {a b : ℤ} (h : a = b) :
a - b = 0
source
@[protected]
theorem int.eq_of_sub_eq_zero {a b : ℤ} (h : a - b = 0) :
a = b
source
@[protected]
theorem int.sub_eq_zero_iff_eq {a b : ℤ} :
a - b = 0 ↔ a = b
source
@[protected, simp]
theorem int.neg_eq_of_add_eq_zero {a b : ℤ} (h : a + b = 0) :
-a = b
source
@[protected]
theorem int.neg_mul_eq_neg_mul (a b : ℤ) :
-(a * b) = -a * b
source
@[protected]
theorem int.neg_mul_eq_mul_neg (a b : ℤ) :
-(a * b) = a * -b
source
theorem int.neg_mul_eq_neg_mul_symm (a b : ℤ) :
-a * b = -(a * b)
source
theorem int.mul_neg_eq_neg_mul_symm (a b : ℤ) :
a * -b = -(a * b)
source
@[protected]
theorem int.neg_mul_neg (a b : ℤ) :
-a * -b = a * b
source
@[protected]
theorem int.neg_mul_comm (a b : ℤ) :
-a * b = a * -b
source
@[protected]
theorem int.mul_sub (a b c : ℤ) :
a * (b - c) = a * b - a * c
source
@[protected]
theorem int.sub_mul (a b c : ℤ) :
(a - b) * c = a * c - b * c
source
@[protected]
theorem int.le_of_add_le_add_left {a b c : ℤ} (h : a + b ≤ a + c) :
b ≤ c
source
@[protected]
theorem int.lt_of_add_lt_add_left {a b c : ℤ} (h : a + b < a + c) :
b < c
source
@[protected]
theorem int.add_le_add_right {a b : ℤ} (h : a ≤ b) (c : ℤ) :
a + c ≤ b + c
source
@[protected]
theorem int.add_lt_add_right {a b : ℤ} (h : a < b) (c : ℤ) :
a + c < b + c
source
@[protected]
theorem int.add_le_add {a b c d : ℤ} (h₁ : a ≤ b) (h₂ : c ≤ d) :
a + c ≤ b + d
source
@[protected]
theorem int.le_add_of_nonneg_right {a b : ℤ} (h : 0 ≤ b) :
a ≤ a + b
source
@[protected]
theorem int.le_add_of_nonneg_left {a b : ℤ} (h : 0 ≤ b) :
a ≤ b + a
source
@[protected]
theorem int.add_lt_add {a b c d : ℤ} (h₁ : a < b) (h₂ : c < d) :
a + c < b + d
source
@[protected]
theorem int.add_lt_add_of_le_of_lt {a b c d : ℤ} (h₁ : a ≤ b) (h₂ : c < d) :
a + c < b + d
source
@[protected]
theorem int.add_lt_add_of_lt_of_le {a b c d : ℤ} (h₁ : a < b) (h₂ : c ≤ d) :
a + c < b + d
source
@[protected]
theorem int.lt_add_of_pos_right (a : ℤ) {b : ℤ} (h : 0 < b) :
a < a + b
source
@[protected]
theorem int.lt_add_of_pos_left (a : ℤ) {b : ℤ} (h : 0 < b) :
a < b + a
source
@[protected]
theorem int.le_of_add_le_add_right {a b c : ℤ} (h : a + b ≤ c + b) :
a ≤ c
source
@[protected]
theorem int.lt_of_add_lt_add_right {a b c : ℤ} (h : a + b < c + b) :
a < c
source
@[protected]
theorem int.add_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) :
0 ≤ a + b
source
@[protected]
theorem int.add_pos {a b : ℤ} (ha : 0 < a) (hb : 0 < b) :
0 < a + b
source
@[protected]
theorem int.add_pos_of_pos_of_nonneg {a b : ℤ} (ha : 0 < a) (hb : 0 ≤ b) :
0 < a + b
source
@[protected]
theorem int.add_pos_of_nonneg_of_pos {a b : ℤ} (ha : 0 ≤ a) (hb : 0 < b) :
0 < a + b
source
@[protected]
theorem int.add_nonpos {a b : ℤ} (ha : a ≤ 0) (hb : b ≤ 0) :
a + b ≤ 0
source
@[protected]
theorem int.add_neg {a b : ℤ} (ha : a < 0) (hb : b < 0) :
a + b < 0
source
@[protected]
theorem int.add_neg_of_neg_of_nonpos {a b : ℤ} (ha : a < 0) (hb : b ≤ 0) :
a + b < 0
source
@[protected]
theorem int.add_neg_of_nonpos_of_neg {a b : ℤ} (ha : a ≤ 0) (hb : b < 0) :
a + b < 0
source
@[protected]
theorem int.lt_add_of_le_of_pos {a b c : ℤ} (hbc : b ≤ c) (ha : 0 < a) :
b < c + a
source
@[protected]
theorem int.sub_add_cancel (a b : ℤ) :
a - b + b = a
source
@[protected]
theorem int.add_sub_cancel (a b : ℤ) :
a + b - b = a
source
@[protected]
theorem int.add_sub_assoc (a b c : ℤ) :
a + b - c = a + (b - c)
source
@[protected]
theorem int.neg_le_neg {a b : ℤ} (h : a ≤ b) :
-b ≤ -a
source
@[protected]
theorem int.le_of_neg_le_neg {a b : ℤ} (h : -b ≤ -a) :
a ≤ b
source
@[protected]
theorem int.nonneg_of_neg_nonpos {a : ℤ} (h : -a ≤ 0) :
0 ≤ a
source
@[protected]
theorem int.neg_nonpos_of_nonneg {a : ℤ} (h : 0 ≤ a) :
-a ≤ 0
source
@[protected]
theorem int.nonpos_of_neg_nonneg {a : ℤ} (h : 0 ≤ -a) :
a ≤ 0
source
@[protected]
theorem int.neg_nonneg_of_nonpos {a : ℤ} (h : a ≤ 0) :
0 ≤ -a
source
@[protected]
theorem int.neg_lt_neg {a b : ℤ} (h : a < b) :
-b < -a
source
@[protected]
theorem int.lt_of_neg_lt_neg {a b : ℤ} (h : -b < -a) :
a < b
source
@[protected]
theorem int.pos_of_neg_neg {a : ℤ} (h : -a < 0) :
0 < a
source
@[protected]
theorem int.neg_neg_of_pos {a : ℤ} (h : 0 < a) :
-a < 0
source
@[protected]
theorem int.neg_of_neg_pos {a : ℤ} (h : 0 < -a) :
a < 0
source
@[protected]
theorem int.neg_pos_of_neg {a : ℤ} (h : a < 0) :
0 < -a
source
@[protected]
theorem int.le_neg_of_le_neg {a b : ℤ} (h : a ≤ -b) :
b ≤ -a
source
@[protected]
theorem int.neg_le_of_neg_le {a b : ℤ} (h : -a ≤ b) :
-b ≤ a
source
@[protected]
theorem int.lt_neg_of_lt_neg {a b : ℤ} (h : a < -b) :
b < -a
source
@[protected]
theorem int.neg_lt_of_neg_lt {a b : ℤ} (h : -a < b) :
-b < a
source
@[protected]
theorem int.sub_nonneg_of_le {a b : ℤ} (h : b ≤ a) :
0 ≤ a - b
source
@[protected]
theorem int.le_of_sub_nonneg {a b : ℤ} (h : 0 ≤ a - b) :
b ≤ a
source
@[protected]
theorem int.sub_nonpos_of_le {a b : ℤ} (h : a ≤ b) :
a - b ≤ 0
source
@[protected]
theorem int.le_of_sub_nonpos {a b : ℤ} (h : a - b ≤ 0) :
a ≤ b
source
@[protected]
theorem int.sub_pos_of_lt {a b : ℤ} (h : b < a) :
0 < a - b
source
@[protected]
theorem int.lt_of_sub_pos {a b : ℤ} (h : 0 < a - b) :
b < a
source
@[protected]
theorem int.sub_neg_of_lt {a b : ℤ} (h : a < b) :
a - b < 0
source
@[protected]
theorem int.lt_of_sub_neg {a b : ℤ} (h : a - b < 0) :
a < b
source
@[protected]
theorem int.add_le_of_le_neg_add {a b c : ℤ} (h : b ≤ -a + c) :
a + b ≤ c
source
@[protected]
theorem int.le_neg_add_of_add_le {a b c : ℤ} (h : a + b ≤ c) :
b ≤ -a + c
source
@[protected]
theorem int.add_le_of_le_sub_left {a b c : ℤ} (h : b ≤ c - a) :
a + b ≤ c
source
@[protected]
theorem int.le_sub_left_of_add_le {a b c : ℤ} (h : a + b ≤ c) :
b ≤ c - a
source
@[protected]
theorem int.add_le_of_le_sub_right {a b c : ℤ} (h : a ≤ c - b) :
a + b ≤ c
source
@[protected]
theorem int.le_sub_right_of_add_le {a b c : ℤ} (h : a + b ≤ c) :
a ≤ c - b
source
@[protected]
theorem int.le_add_of_neg_add_le {a b c : ℤ} (h : -b + a ≤ c) :
a ≤ b + c
source
@[protected]
theorem int.neg_add_le_of_le_add {a b c : ℤ} (h : a ≤ b + c) :
-b + a ≤ c
source
@[protected]
theorem int.le_add_of_sub_left_le {a b c : ℤ} (h : a - b ≤ c) :
a ≤ b + c
source
@[protected]
theorem int.sub_left_le_of_le_add {a b c : ℤ} (h : a ≤ b + c) :
a - b ≤ c
source
@[protected]
theorem int.le_add_of_sub_right_le {a b c : ℤ} (h : a - c ≤ b) :
a ≤ b + c
source
@[protected]
theorem int.sub_right_le_of_le_add {a b c : ℤ} (h : a ≤ b + c) :
a - c ≤ b
source
@[protected]
theorem int.le_add_of_neg_add_le_left {a b c : ℤ} (h : -b + a ≤ c) :
a ≤ b + c
source
@[protected]
theorem int.neg_add_le_left_of_le_add {a b c : ℤ} (h : a ≤ b + c) :
-b + a ≤ c
source
@[protected]
theorem int.le_add_of_neg_add_le_right {a b c : ℤ} (h : -c + a ≤ b) :
a ≤ b + c
source
@[protected]
theorem int.neg_add_le_right_of_le_add {a b c : ℤ} (h : a ≤ b + c) :
-c + a ≤ b
source
@[protected]
theorem int.le_add_of_neg_le_sub_left {a b c : ℤ} (h : -a ≤ b - c) :
c ≤ a + b
source
@[protected]
theorem int.neg_le_sub_left_of_le_add {a b c : ℤ} (h : c ≤ a + b) :
-a ≤ b - c
source
@[protected]
theorem int.le_add_of_neg_le_sub_right {a b c : ℤ} (h : -b ≤ a - c) :
c ≤ a + b
source
@[protected]
theorem int.neg_le_sub_right_of_le_add {a b c : ℤ} (h : c ≤ a + b) :
-b ≤ a - c
source
@[protected]
theorem int.sub_le_of_sub_le {a b c : ℤ} (h : a - b ≤ c) :
a - c ≤ b
source
@[protected]
theorem int.sub_le_sub_left {a b : ℤ} (h : a ≤ b) (c : ℤ) :
c - b ≤ c - a
source
@[protected]
theorem int.sub_le_sub_right {a b : ℤ} (h : a ≤ b) (c : ℤ) :
a - c ≤ b - c
source
@[protected]
theorem int.sub_le_sub {a b c d : ℤ} (hab : a ≤ b) (hcd : c ≤ d) :
a - d ≤ b - c
source
@[protected]
theorem int.add_lt_of_lt_neg_add {a b c : ℤ} (h : b < -a + c) :
a + b < c
source
@[protected]
theorem int.lt_neg_add_of_add_lt {a b c : ℤ} (h : a + b < c) :
b < -a + c
source
@[protected]
theorem int.add_lt_of_lt_sub_left {a b c : ℤ} (h : b < c - a) :
a + b < c
source
@[protected]
theorem int.lt_sub_left_of_add_lt {a b c : ℤ} (h : a + b < c) :
b < c - a
source
@[protected]
theorem int.add_lt_of_lt_sub_right {a b c : ℤ} (h : a < c - b) :
a + b < c
source
@[protected]
theorem int.lt_sub_right_of_add_lt {a b c : ℤ} (h : a + b < c) :
a < c - b
source
@[protected]
theorem int.lt_add_of_neg_add_lt {a b c : ℤ} (h : -b + a < c) :
a < b + c
source
@[protected]
theorem int.neg_add_lt_of_lt_add {a b c : ℤ} (h : a < b + c) :
-b + a < c
source
@[protected]
theorem int.lt_add_of_sub_left_lt {a b c : ℤ} (h : a - b < c) :
a < b + c
source
@[protected]
theorem int.sub_left_lt_of_lt_add {a b c : ℤ} (h : a < b + c) :
a - b < c
source
@[protected]
theorem int.lt_add_of_sub_right_lt {a b c : ℤ} (h : a - c < b) :
a < b + c
source
@[protected]
theorem int.sub_right_lt_of_lt_add {a b c : ℤ} (h : a < b + c) :
a - c < b
source
@[protected]
theorem int.lt_add_of_neg_add_lt_left {a b c : ℤ} (h : -b + a < c) :
a < b + c
source
@[protected]
theorem int.neg_add_lt_left_of_lt_add {a b c : ℤ} (h : a < b + c) :
-b + a < c
source
@[protected]
theorem int.lt_add_of_neg_add_lt_right {a b c : ℤ} (h : -c + a < b) :
a < b + c
source
@[protected]
theorem int.neg_add_lt_right_of_lt_add {a b c : ℤ} (h : a < b + c) :
-c + a < b
source
@[protected]
theorem int.lt_add_of_neg_lt_sub_left {a b c : ℤ} (h : -a < b - c) :
c < a + b
source
@[protected]
theorem int.neg_lt_sub_left_of_lt_add {a b c : ℤ} (h : c < a + b) :
-a < b - c
source
@[protected]
theorem int.lt_add_of_neg_lt_sub_right {a b c : ℤ} (h : -b < a - c) :
c < a + b
source
@[protected]
theorem int.neg_lt_sub_right_of_lt_add {a b c : ℤ} (h : c < a + b) :
-b < a - c
source
@[protected]
theorem int.sub_lt_of_sub_lt {a b c : ℤ} (h : a - b < c) :
a - c < b
source
@[protected]
theorem int.sub_lt_sub_left {a b : ℤ} (h : a < b) (c : ℤ) :
c - b < c - a
source
@[protected]
theorem int.sub_lt_sub_right {a b : ℤ} (h : a < b) (c : ℤ) :
a - c < b - c
source
@[protected]
theorem int.sub_lt_sub {a b c d : ℤ} (hab : a < b) (hcd : c < d) :
a - d < b - c
source
@[protected]
theorem int.sub_lt_sub_of_le_of_lt {a b c d : ℤ} (hab : a ≤ b) (hcd : c < d) :
a - d < b - c
source
@[protected]
theorem int.sub_lt_sub_of_lt_of_le {a b c d : ℤ} (hab : a < b) (hcd : c ≤ d) :
a - d < b - c
source
@[protected]
theorem int.sub_le_self (a : ℤ) {b : ℤ} (h : 0 ≤ b) :
a - b ≤ a
source
@[protected]
theorem int.sub_lt_self (a : ℤ) {b : ℤ} (h : 0 < b) :
a - b < a
source
@[protected]
theorem int.add_le_add_three {a b c d e f : ℤ} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) :
a + b + c ≤ d + e + f

missing facts

source
@[protected]
theorem int.mul_lt_mul_of_pos_left {a b c : ℤ} (h₁ : a < b) (h₂ : 0 < c) :
c * a < c * b
source
@[protected]
theorem int.mul_lt_mul_of_pos_right {a b c : ℤ} (h₁ : a < b) (h₂ : 0 < c) :
a * c < b * c
source
@[protected]
theorem int.mul_le_mul_of_nonneg_left {a b c : ℤ} (h₁ : a ≤ b) (h₂ : 0 ≤ c) :
c * a ≤ c * b
source
@[protected]
theorem int.mul_le_mul_of_nonneg_right {a b c : ℤ} (h₁ : a ≤ b) (h₂ : 0 ≤ c) :
a * c ≤ b * c
source
@[protected]
theorem int.mul_le_mul {a b c d : ℤ} (hac : a ≤ c) (hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) :
a * b ≤ c * d
source
@[protected]
theorem int.mul_nonpos_of_nonneg_of_nonpos {a b : ℤ} (ha : 0 ≤ a) (hb : b ≤ 0) :
a * b ≤ 0
source
@[protected]
theorem int.mul_nonpos_of_nonpos_of_nonneg {a b : ℤ} (ha : a ≤ 0) (hb : 0 ≤ b) :
a * b ≤ 0
source
@[protected]
theorem int.mul_lt_mul {a b c d : ℤ} (hac : a < c) (hbd : b ≤ d) (pos_b : 0 < b) (nn_c : 0 ≤ c) :
a * b < c * d
source
@[protected]
theorem int.mul_lt_mul' {a b c d : ℤ} (h1 : a ≤ c) (h2 : b < d) (h3 : 0 ≤ b) (h4 : 0 < c) :
a * b < c * d
source
@[protected]
theorem int.mul_neg_of_pos_of_neg {a b : ℤ} (ha : 0 < a) (hb : b < 0) :
a * b < 0
source
@[protected]
theorem int.mul_neg_of_neg_of_pos {a b : ℤ} (ha : a < 0) (hb : 0 < b) :
a * b < 0
source
@[protected]
theorem int.mul_le_mul_of_nonpos_right {a b c : ℤ} (h : b ≤ a) (hc : c ≤ 0) :
a * c ≤ b * c
source
@[protected]
theorem int.mul_nonneg_of_nonpos_of_nonpos {a b : ℤ} (ha : a ≤ 0) (hb : b ≤ 0) :
0 ≤ a * b
source
@[protected]
theorem int.mul_lt_mul_of_neg_left {a b c : ℤ} (h : b < a) (hc : c < 0) :
c * a < c * b
source
@[protected]
theorem int.mul_lt_mul_of_neg_right {a b c : ℤ} (h : b < a) (hc : c < 0) :
a * c < b * c
source
@[protected]
theorem int.mul_pos_of_neg_of_neg {a b : ℤ} (ha : a < 0) (hb : b < 0) :
0 < a * b
source
@[protected]
theorem int.mul_self_le_mul_self {a b : ℤ} (h1 : 0 ≤ a) (h2 : a ≤ b) :
a * a ≤ b * b
source
@[protected]
theorem int.mul_self_lt_mul_self {a b : ℤ} (h1 : 0 ≤ a) (h2 : a < b) :
a * a < b * b

more facts specific to int

source
theorem int.of_nat_nonneg (n : ℕ) :
0 ≤ int.of_nat n
source
theorem int.coe_succ_pos (n : ℕ) :
0 < ↑(n.succ)
source
theorem int.exists_eq_neg_of_nat {a : ℤ} (H : a ≤ 0) :
∃ (n : ℕ), a = -↑n
source
theorem int.nat_abs_of_nonneg {a : ℤ} (H : 0 ≤ a) :
↑(a.nat_abs) = a
source
theorem int.of_nat_nat_abs_of_nonpos {a : ℤ} (H : a ≤ 0) :
↑(a.nat_abs) = -a
source
theorem int.lt_of_add_one_le {a b : ℤ} (H : a + 1 ≤ b) :
a < b
source
theorem int.add_one_le_of_lt {a b : ℤ} (H : a < b) :
a + 1 ≤ b
source
theorem int.lt_add_one_of_le {a b : ℤ} (H : a ≤ b) :
a < b + 1
source
theorem int.le_of_lt_add_one {a b : ℤ} (H : a < b + 1) :
a ≤ b
source
theorem int.sub_one_lt_of_le {a b : ℤ} (H : a ≤ b) :
a - 1 < b
source
theorem int.le_of_sub_one_lt {a b : ℤ} (H : a - 1 < b) :
a ≤ b
source
theorem int.le_sub_one_of_lt {a b : ℤ} (H : a < b) :
a ≤ b - 1
source
theorem int.lt_of_le_sub_one {a b : ℤ} (H : a ≤ b - 1) :
a < b
source
theorem int.sign_of_succ (n : ℕ) :
↑(n.succ).sign = 1
source
theorem int.sign_eq_one_of_pos {a : ℤ} (h : 0 < a) :
a.sign = 1
source
theorem int.sign_eq_neg_one_of_neg {a : ℤ} (h : a < 0) :
a.sign = -1
source
theorem int.eq_zero_of_sign_eq_zero {a : ℤ} :
a.sign = 0 → a = 0
source
theorem int.pos_of_sign_eq_one {a : ℤ} :
a.sign = 1 → 0 < a
source
theorem int.neg_of_sign_eq_neg_one {a : ℤ} :
a.sign = -1 → a < 0
source
theorem int.sign_eq_one_iff_pos (a : ℤ) :
a.sign = 1 ↔ 0 < a
source
theorem int.sign_eq_neg_one_iff_neg (a : ℤ) :
a.sign = -1 ↔ a < 0
source
theorem int.sign_eq_zero_iff_zero (a : ℤ) :
a.sign = 0 ↔ a = 0
source
@[protected]
theorem int.eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} (h : a * b = 0) :
a = 0 ∨ b = 0
source
@[protected]
theorem int.eq_of_mul_eq_mul_right {a b c : ℤ} (ha : a ≠ 0) (h : b * a = c * a) :
b = c
source
@[protected]
theorem int.eq_of_mul_eq_mul_left {a b c : ℤ} (ha : a ≠ 0) (h : a * b = a * c) :
b = c
source
theorem int.eq_one_of_mul_eq_self_left {a b : ℤ} (Hpos : a ≠ 0) (H : b * a = a) :
b = 1
source
theorem int.eq_one_of_mul_eq_self_right {a b : ℤ} (Hpos : b ≠ 0) (H : b * a = b) :
a = 1