# mathlibdocumentation

core / init.data.int.basic

inductive int  :
Type
Instances for int
@[protected, instance]
@[protected, instance]
def int.has_coe  :
Equations
@[protected]
def int.repr  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
theorem int.coe_nat_eq (n : ) :
n =
@[protected]
def int.zero  :
Equations
@[protected]
def int.one  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def int.has_one  :
Equations
theorem int.of_nat_zero  :
= 0
theorem int.of_nat_one  :
= 1
def int.neg_of_nat  :
Equations
def int.sub_nat_nat (m n : ) :
Equations
• = int.sub_nat_nat._match_1 m n (n - m)
• int.sub_nat_nat._match_1 m n k.succ =
• int.sub_nat_nat._match_1 m n 0 = int.of_nat (m - n)
theorem int.sub_nat_nat_of_sub_eq_zero {m n : } (h : n - m = 0) :
= int.of_nat (m - n)
theorem int.sub_nat_nat_of_sub_eq_succ {m n k : } (h : n - m = k.succ) :
=
@[protected]
def int.neg  :
Equations
@[protected]
Equations
@[protected]
def int.mul  :
Equations
@[protected, instance]
def int.has_neg  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def int.has_mul  :
Equations
@[protected]
def int.sub  :
Equations
@[protected, instance]
def int.has_sub  :
Equations
@[protected]
theorem int.neg_zero  :
-0 = 0
theorem int.of_nat_add (n m : ) :
int.of_nat (n + m) =
theorem int.of_nat_mul (n m : ) :
int.of_nat (n * m) =
theorem int.of_nat_succ (n : ) :
= + 1
theorem int.neg_of_nat_zero  :
= 0
theorem int.neg_of_nat_of_succ (n : ) :
@[simp]
theorem int.of_nat_eq_coe (n : ) :
= n
theorem int.neg_succ_of_nat_coe (n : ) :
= -(n + 1)
@[protected]
theorem int.coe_nat_add (m n : ) :
(m + n) = m + n
@[protected]
theorem int.coe_nat_mul (m n : ) :
(m * n) = m * n
@[protected]
theorem int.coe_nat_zero  :
0 = 0
@[protected]
theorem int.coe_nat_one  :
1 = 1
@[protected]
theorem int.coe_nat_succ (n : ) :
(n.succ) = n + 1
@[protected]
theorem int.coe_nat_add_out (m n : ) :
m + n = m + n
@[protected]
theorem int.coe_nat_mul_out (m n : ) :
m * n = (m * n)
@[protected]
theorem int.coe_nat_add_one_out (n : ) :
n + 1 = (n.succ)
theorem int.of_nat_add_of_nat (m n : ) :
= int.of_nat (m + n)
theorem int.of_nat_mul_of_nat (m n : ) :
= int.of_nat (m * n)
@[protected]
theorem int.coe_nat_inj {m n : } (h : m = n) :
m = n
theorem int.of_nat_eq_of_nat_iff (m n : ) :
m = n
@[protected]
theorem int.coe_nat_eq_coe_nat_iff (m n : ) :
m = n m = n
theorem int.neg_succ_of_nat_inj_iff {m n : } :
= m = n
theorem int.neg_succ_of_nat_eq (n : ) :
= -(n + 1)
@[protected]
theorem int.neg_neg (a : ) :
--a = a
@[protected]
theorem int.neg_inj {a b : } (h : -a = -b) :
a = b
@[protected]
theorem int.sub_eq_add_neg {a b : } :
a - b = a + -b
theorem int.sub_nat_nat_elim (m n : ) (P : → Prop) (hp : ∀ (i n : ), P (n + i) n (int.of_nat i)) (hn : ∀ (i m : ), P m (m + i + 1) ) :
P m n n)
theorem int.sub_nat_nat_add_left {m n : } :
theorem int.sub_nat_nat_add_right {m n : } :
(m + n + 1) =
theorem int.sub_nat_nat_add_add (m n k : ) :
int.sub_nat_nat (m + k) (n + k) =
theorem int.sub_nat_nat_of_le {m n : } (h : n m) :
= int.of_nat (m - n)
theorem int.sub_nat_nat_of_lt {m n : } (h : m < n) :
= -[1+ (n - m).pred]
@[simp]
def int.nat_abs  :
Equations
@[simp, norm_cast]
theorem int.nat_abs_of_nat (n : ) :
theorem int.eq_zero_of_nat_abs_eq_zero {a : } :
a.nat_abs = 0a = 0
theorem int.nat_abs_pos_of_ne_zero {a : } (h : a 0) :
@[simp]
theorem int.nat_abs_zero  :
@[simp]
theorem int.nat_abs_one  :
theorem int.nat_abs_mul_self {a : } :
(a.nat_abs * a.nat_abs) = a * a
@[simp]
theorem int.nat_abs_neg (a : ) :
theorem int.nat_abs_eq (a : ) :
theorem int.eq_coe_or_neg (a : ) :
∃ (n : ), a = n a = -n
def int.sign  :
Equations
@[simp]
theorem int.sign_zero  :
0.sign = 0
@[simp]
theorem int.sign_one  :
1.sign = 1
@[simp]
theorem int.sign_neg_one  :
(-1).sign = -1
@[protected]
def int.div  :
Equations
@[protected]
def int.mod  :
Equations
def int.fdiv  :
Equations
def int.fmod  :
Equations
def int.quot  :
Equations
def int.rem  :
Equations
@[protected, instance]
def int.has_div  :
Equations
@[protected, instance]
def int.has_mod  :
Equations
def int.gcd (m n : ) :
Equations
@[protected]
theorem int.add_comm (a b : ) :
a + b = b + a
@[protected]
theorem int.add_zero (a : ) :
a + 0 = a
@[protected]
theorem int.zero_add (a : ) :
0 + a = a
theorem int.sub_nat_nat_sub {m n : } (h : n m) (k : ) :
int.sub_nat_nat (m - n) k = (k + n)
theorem int.sub_nat_nat_add (m n k : ) :
theorem int.sub_nat_nat_add_neg_succ_of_nat (m n k : ) :
+ = (n + k.succ)
theorem int.add_assoc_aux1 (m n : ) (c : ) :
+ c = + + c)
theorem int.add_assoc_aux2 (m n k : ) :
+ + = + (-[1+ n] +
@[protected]
theorem int.add_assoc (a b c : ) :
a + b + c = a + (b + c)
theorem int.sub_nat_self (n : ) :
= 0
@[protected]
theorem int.add_left_neg (a : ) :
-a + a = 0
@[protected]
theorem int.add_right_neg (a : ) :
a + -a = 0
@[protected]
theorem int.mul_comm (a b : ) :
a * b = b * a
@[protected]
theorem int.mul_assoc (a b c : ) :
a * b * c = a * (b * c)
@[protected]
theorem int.mul_zero (a : ) :
a * 0 = 0
@[protected]
theorem int.zero_mul (a : ) :
0 * a = 0
theorem int.of_nat_mul_sub_nat_nat (m n k : ) :
= int.sub_nat_nat (m * n) (m * k)
theorem int.neg_of_nat_add (m n : ) :
@[protected]
theorem int.distrib_left (a b c : ) :
a * (b + c) = a * b + a * c
@[protected]
theorem int.distrib_right (a b c : ) :
(a + b) * c = a * c + b * c
@[protected]
theorem int.zero_ne_one  :
0 1
theorem int.of_nat_sub {n m : } (h : m n) :
int.of_nat (n - m) =
@[protected]
theorem int.add_left_comm (a b c : ) :
a + (b + c) = b + (a + c)
@[protected]
theorem int.add_left_cancel {a b c : } (h : a + b = a + c) :
b = c
@[protected]
theorem int.neg_add {a b : } :
-(a + b) = -a + -b
theorem int.neg_succ_of_nat_coe' (n : ) :
= -n - 1
@[protected]
theorem int.coe_nat_sub {n m : } :
n m(m - n) = m - n
@[protected]
theorem int.sub_nat_nat_eq_coe {m n : } :
= m - n
def int.to_nat  :
Equations
theorem int.to_nat_sub (m n : ) :
(m - n).to_nat = m - n
def int.nat_mod (m n : ) :
Equations
@[protected]
theorem int.one_mul (a : ) :
1 * a = a
@[protected]
theorem int.mul_one (a : ) :
a * 1 = a
@[protected]
theorem int.neg_eq_neg_one_mul (a : ) :
-a = (-1) * a
theorem int.sign_mul_nat_abs (a : ) :
a.sign * (a.nat_abs) = a