mathlib3 documentation

core / init.data.int.basic

The integers, with addition, multiplication, and subtraction. #

the type, coercions, and notation

source
inductive int  :
Type
Instances for int
source
@[protected, instance]
def int.decidable_eq  :
decidable_eq ℤ
source
@[protected, instance]
def int.has_coe  :
has_coe ℕ ℤ
Equations
source
@[protected]
def int.repr  :
ℤ → string
Equations
source
@[protected, instance]
def int.has_repr  :
has_repr ℤ
Equations
source
@[protected, instance]
def int.has_to_string  :
has_to_string ℤ
Equations
source
@[protected]
theorem int.coe_nat_eq (n : ℕ) :
↑n = int.of_nat n
source
@[protected]
def int.zero  :
ℤ
Equations
source
@[protected]
def int.one  :
ℤ
Equations
source
@[protected, instance]
def int.has_zero  :
has_zero ℤ
Equations
source
@[protected, instance]
def int.has_one  :
has_one ℤ
Equations
source
theorem int.of_nat_zero  :
int.of_nat 0 = 0
source
theorem int.of_nat_one  :
int.of_nat 1 = 1

definitions of basic functions

source
def int.neg_of_nat  :
ℕ → ℤ
Equations
source
def int.sub_nat_nat (m n : ℕ) :
ℤ
Equations
source
theorem int.sub_nat_nat_of_sub_eq_zero {m n : ℕ} (h : n - m = 0) :
int.sub_nat_nat m n = int.of_nat (m - n)
source
theorem int.sub_nat_nat_of_sub_eq_succ {m n k : ℕ} (h : n - m = k.succ) :
int.sub_nat_nat m n = -[1+ k]
source
@[protected]
def int.neg  :
ℤ → ℤ
Equations
source
@[protected]
def int.add  :
ℤ → ℤ → ℤ
Equations
source
@[protected]
def int.mul  :
ℤ → ℤ → ℤ
Equations
source
@[protected, instance]
def int.has_neg  :
has_neg ℤ
Equations
source
@[protected, instance]
def int.has_add  :
has_add ℤ
Equations
source
@[protected, instance]
def int.has_mul  :
has_mul ℤ
Equations
source
@[protected]
def int.sub  :
ℤ → ℤ → ℤ
Equations
source
@[protected, instance]
def int.has_sub  :
has_sub ℤ
Equations
source
@[protected]
theorem int.neg_zero  :
-0 = 0
source
theorem int.of_nat_add (n m : ℕ) :
int.of_nat (n + m) = int.of_nat n + int.of_nat m
source
theorem int.of_nat_mul (n m : ℕ) :
int.of_nat (n * m) = int.of_nat n * int.of_nat m
source
theorem int.of_nat_succ (n : ℕ) :
int.of_nat n.succ = int.of_nat n + 1
source
theorem int.neg_of_nat_zero  :
-int.of_nat 0 = 0
source
theorem int.neg_of_nat_of_succ (n : ℕ) :
-int.of_nat n.succ = -[1+ n]
source
theorem int.neg_neg_of_nat_succ (n : ℕ) :
--[1+ n] = int.of_nat n.succ
source
@[simp]
theorem int.of_nat_eq_coe (n : ℕ) :
int.of_nat n = ↑n
source
theorem int.neg_succ_of_nat_coe (n : ℕ) :
-[1+ n] = -↑(n + 1)
source
@[protected]
theorem int.coe_nat_add (m n : ℕ) :
↑(m + n) = ↑m + ↑n
source
@[protected]
theorem int.coe_nat_mul (m n : ℕ) :
↑(m * n) = ↑m * ↑n
source
@[protected]
theorem int.coe_nat_zero  :
↑0 = 0
source
@[protected]
theorem int.coe_nat_one  :
↑1 = 1
source
@[protected]
theorem int.coe_nat_succ (n : ℕ) :
↑(n.succ) = ↑n + 1
source
@[protected]
theorem int.coe_nat_add_out (m n : ℕ) :
↑m + ↑n = ↑m + ↑n
source
@[protected]
theorem int.coe_nat_mul_out (m n : ℕ) :
↑m * ↑n = ↑(m * n)
source
@[protected]
theorem int.coe_nat_add_one_out (n : ℕ) :
↑n + 1 = ↑(n.succ)

these are only for internal use

source
theorem int.of_nat_add_of_nat (m n : ℕ) :
int.of_nat m + int.of_nat n = int.of_nat (m + n)
source
theorem int.of_nat_add_neg_succ_of_nat (m n : ℕ) :
int.of_nat m + -[1+ n] = int.sub_nat_nat m n.succ
source
theorem int.neg_succ_of_nat_add_of_nat (m n : ℕ) :
-[1+ m] + int.of_nat n = int.sub_nat_nat n m.succ
source
theorem int.neg_succ_of_nat_add_neg_succ_of_nat (m n : ℕ) :
-[1+ m] + -[1+ n] = -[1+ (m + n).succ]
source
theorem int.of_nat_mul_of_nat (m n : ℕ) :
int.of_nat m * int.of_nat n = int.of_nat (m * n)
source
theorem int.of_nat_mul_neg_succ_of_nat (m n : ℕ) :
int.of_nat m * -[1+ n] = int.neg_of_nat (m * n.succ)
source
theorem int.neg_succ_of_nat_of_nat (m n : ℕ) :
-[1+ m] * int.of_nat n = int.neg_of_nat (m.succ * n)
source
theorem int.mul_neg_succ_of_nat_neg_succ_of_nat (m n : ℕ) :
-[1+ m] * -[1+ n] = int.of_nat (m.succ * n.succ)

some basic functions and properties

source
@[protected]
theorem int.coe_nat_inj {m n : ℕ} (h : ↑m = ↑n) :
m = n
source
theorem int.of_nat_eq_of_nat_iff (m n : ℕ) :
int.of_nat m = int.of_nat n ↔ m = n
source
@[protected]
theorem int.coe_nat_eq_coe_nat_iff (m n : ℕ) :
↑m = ↑n ↔ m = n
source
theorem int.neg_succ_of_nat_inj_iff {m n : ℕ} :
-[1+ m] = -[1+ n] ↔ m = n
source
theorem int.neg_succ_of_nat_eq (n : ℕ) :
-[1+ n] = -(↑n + 1)

neg

source
@[protected]
theorem int.neg_neg (a : ℤ) :
--a = a
source
@[protected]
theorem int.neg_inj {a b : ℤ} (h : -a = -b) :
a = b
source
@[protected]
theorem int.sub_eq_add_neg {a b : ℤ} :
a - b = a + -b

basic properties of sub_nat_nat

source
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) -[1+ i]) :
P m n (int.sub_nat_nat m n)
source
theorem int.sub_nat_nat_add_left {m n : ℕ} :
int.sub_nat_nat (m + n) m = int.of_nat n
source
theorem int.sub_nat_nat_add_right {m n : ℕ} :
int.sub_nat_nat m (m + n + 1) = -[1+ n]
source
theorem int.sub_nat_nat_add_add (m n k : ℕ) :
int.sub_nat_nat (m + k) (n + k) = int.sub_nat_nat m n
source
theorem int.sub_nat_nat_of_le {m n : ℕ} (h : n ≤ m) :
int.sub_nat_nat m n = int.of_nat (m - n)
source
theorem int.sub_nat_nat_of_lt {m n : ℕ} (h : m < n) :
int.sub_nat_nat m n = -[1+ (n - m).pred]

nat_abs

source
@[simp]
def int.nat_abs  :
ℤ → ℕ
Equations
source
@[simp, norm_cast]
theorem int.nat_abs_of_nat (n : ℕ) :
↑n.nat_abs = n
source
theorem int.eq_zero_of_nat_abs_eq_zero {a : ℤ} :
a.nat_abs = 0 → a = 0
source
theorem int.nat_abs_pos_of_ne_zero {a : ℤ} (h : a ≠ 0) :
0 < a.nat_abs
source
@[simp]
theorem int.nat_abs_zero  :
0.nat_abs = 0
source
@[simp]
theorem int.nat_abs_one  :
1.nat_abs = 1
source
theorem int.nat_abs_mul_self {a : ℤ} :
↑(a.nat_abs * a.nat_abs) = a * a
source
@[simp]
theorem int.nat_abs_neg (a : ℤ) :
(-a).nat_abs = a.nat_abs
source
theorem int.nat_abs_eq (a : ℤ) :
a = ↑(a.nat_abs) ∨ a = -↑(a.nat_abs)
source
theorem int.eq_coe_or_neg (a : ℤ) :
∃ (n : ℕ), a = ↑n ∨ a = -↑n

sign

source
def int.sign  :
ℤ → ℤ
Equations
source
@[simp]
theorem int.sign_zero  :
0.sign = 0
source
@[simp]
theorem int.sign_one  :
1.sign = 1
source
@[simp]
theorem int.sign_neg_one  :
(-1).sign = -1

Quotient and remainder

source
@[protected]
def int.div  :
ℤ → ℤ → ℤ
Equations
source
@[protected]
def int.mod  :
ℤ → ℤ → ℤ
Equations
source
def int.fdiv  :
ℤ → ℤ → ℤ
Equations
source
def int.fmod  :
ℤ → ℤ → ℤ
Equations
source
def int.quot  :
ℤ → ℤ → ℤ
Equations
source
def int.rem  :
ℤ → ℤ → ℤ
Equations
source
@[protected, instance]
def int.has_div  :
has_div ℤ
Equations
source
@[protected, instance]
def int.has_mod  :
has_mod ℤ
Equations

gcd

source
def int.gcd (m n : ℤ) :
ℕ
Equations

addition

source
@[protected]
theorem int.add_comm (a b : ℤ) :
a + b = b + a
source
@[protected]
theorem int.add_zero (a : ℤ) :
a + 0 = a
source
@[protected]
theorem int.zero_add (a : ℤ) :
0 + a = a
source
theorem int.sub_nat_nat_sub {m n : ℕ} (h : n ≤ m) (k : ℕ) :
int.sub_nat_nat (m - n) k = int.sub_nat_nat m (k + n)
source
theorem int.sub_nat_nat_add (m n k : ℕ) :
int.sub_nat_nat (m + n) k = int.of_nat m + int.sub_nat_nat n k
source
theorem int.sub_nat_nat_add_neg_succ_of_nat (m n k : ℕ) :
int.sub_nat_nat m n + -[1+ k] = int.sub_nat_nat m (n + k.succ)
source
theorem int.add_assoc_aux1 (m n : ℕ) (c : ℤ) :
int.of_nat m + int.of_nat n + c = int.of_nat m + (int.of_nat n + c)
source
theorem int.add_assoc_aux2 (m n k : ℕ) :
-[1+ m] + -[1+ n] + int.of_nat k = -[1+ m] + (-[1+ n] + int.of_nat k)
source
@[protected]
theorem int.add_assoc (a b c : ℤ) :
a + b + c = a + (b + c)

negation

source
theorem int.sub_nat_self (n : ℕ) :
int.sub_nat_nat n n = 0
source
@[protected]
theorem int.add_left_neg (a : ℤ) :
-a + a = 0
source
@[protected]
theorem int.add_right_neg (a : ℤ) :
a + -a = 0

multiplication

source
@[protected]
theorem int.mul_comm (a b : ℤ) :
a * b = b * a
source
theorem int.of_nat_mul_neg_of_nat (m n : ℕ) :
int.of_nat m * int.neg_of_nat n = int.neg_of_nat (m * n)
source
theorem int.neg_of_nat_mul_of_nat (m n : ℕ) :
int.neg_of_nat m * int.of_nat n = int.neg_of_nat (m * n)
source
theorem int.neg_succ_of_nat_mul_neg_of_nat (m n : ℕ) :
-[1+ m] * int.neg_of_nat n = int.of_nat (m.succ * n)
source
theorem int.neg_of_nat_mul_neg_succ_of_nat (m n : ℕ) :
int.neg_of_nat n * -[1+ m] = int.of_nat (n * m.succ)
source
@[protected]
theorem int.mul_assoc (a b c : ℤ) :
a * b * c = a * (b * c)
source
@[protected]
theorem int.mul_zero (a : ℤ) :
a * 0 = 0
source
@[protected]
theorem int.zero_mul (a : ℤ) :
0 * a = 0
source
theorem int.neg_of_nat_eq_sub_nat_nat_zero (n : ℕ) :
int.neg_of_nat n = int.sub_nat_nat 0 n
source
theorem int.of_nat_mul_sub_nat_nat (m n k : ℕ) :
int.of_nat m * int.sub_nat_nat n k = int.sub_nat_nat (m * n) (m * k)
source
theorem int.neg_of_nat_add (m n : ℕ) :
int.neg_of_nat m + int.neg_of_nat n = int.neg_of_nat (m + n)
source
theorem int.neg_succ_of_nat_mul_sub_nat_nat (m n k : ℕ) :
-[1+ m] * int.sub_nat_nat n k = int.sub_nat_nat (m.succ * k) (m.succ * n)
source
@[protected]
theorem int.distrib_left (a b c : ℤ) :
a * (b + c) = a * b + a * c
source
@[protected]
theorem int.distrib_right (a b c : ℤ) :
(a + b) * c = a * c + b * c
source
@[protected]
theorem int.zero_ne_one  :
0 ≠ 1
source
theorem int.of_nat_sub {n m : ℕ} (h : m ≤ n) :
int.of_nat (n - m) = int.of_nat n - int.of_nat m
source
@[protected]
theorem int.add_left_comm (a b c : ℤ) :
a + (b + c) = b + (a + c)
source
@[protected]
theorem int.add_left_cancel {a b c : ℤ} (h : a + b = a + c) :
b = c
source
@[protected]
theorem int.neg_add {a b : ℤ} :
-(a + b) = -a + -b
source
theorem int.neg_succ_of_nat_coe' (n : ℕ) :
-[1+ n] = -↑n - 1
source
@[protected]
theorem int.coe_nat_sub {n m : ℕ} :
n ≤ m → ↑(m - n) = ↑m - ↑n
source
@[protected]
theorem int.sub_nat_nat_eq_coe {m n : ℕ} :
int.sub_nat_nat m n = ↑m - ↑n
source
def int.to_nat  :
ℤ → ℕ
Equations
source
theorem int.to_nat_sub (m n : ℕ) :
(↑m - ↑n).to_nat = m - n
source
def int.nat_mod (m n : ℤ) :
ℕ
Equations
source
@[protected]
theorem int.one_mul (a : ℤ) :
1 * a = a
source
@[protected]
theorem int.mul_one (a : ℤ) :
a * 1 = a
source
@[protected]
theorem int.neg_eq_neg_one_mul (a : ℤ) :
-a = (-1) * a
source
theorem int.sign_mul_nat_abs (a : ℤ) :
a.sign * ↑(a.nat_abs) = a