mathlib documentation

theorem int.sub_nat_nat_add_left {m n : ℕ} :

int.sub_nat_nat (m + n) m = int.of_nat n

theorem int.sub_nat_nat_add_right {m n : ℕ} :

int.sub_nat_nat m (m + n + 1) = -[1+ n]

theorem int.sub_nat_nat_add_add (m n k : ℕ) :

int.sub_nat_nat (m + k) (n + k) = int.sub_nat_nat m n

theorem int.sub_nat_nat_of_ge {m n : ℕ} (h : m ≥ n) :

int.sub_nat_nat m n = int.of_nat (m - n)

theorem int.sub_nat_nat_of_lt {m n : ℕ} (h : m < n) :

int.sub_nat_nat m n = -[1+ (n - m).pred]

@[simp]

def int.nat_abs (a : ℤ) :

Equations

-[1+ m].nat_abs = m.succ
(int.of_nat m).nat_abs = m

@[simp]

theorem int.nat_abs_of_nat (n : ℕ) :

↑n.nat_abs = n

theorem int.eq_zero_of_nat_abs_eq_zero {a : ℤ} (a_1 : a.nat_abs = 0) :

a = 0

theorem int.nat_abs_pos_of_ne_zero {a : ℤ} (h : a ≠ 0) :

a.nat_abs > 0

@[simp]

theorem int.nat_abs_zero :

0.nat_abs = 0

@[simp]

theorem int.nat_abs_one :

1.nat_abs = 1

theorem int.nat_abs_mul_self {a : ℤ} :

↑(a.nat_abs) * a.nat_abs = a * a

@[simp]

theorem int.nat_abs_neg (a : ℤ) :

(-a).nat_abs = a.nat_abs

theorem int.nat_abs_eq (a : ℤ) :

a = ↑(a.nat_abs) ∨ a = -↑(a.nat_abs)

theorem int.eq_coe_or_neg (a : ℤ) :

∃ (n : ℕ), a = ↑n ∨ a = -↑n

def int.sign (a : ℤ) :

Equations

-[1+ n].sign = -1
↑(n + 1).sign = 1
0.sign = 0

@[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

def int.div (a a_1 : ℤ) :

Equations

-[1+ m].div -[1+ n] = int.of_nat (m / n.succ).succ
-[1+ m].div ↑(n + 1) = -[1+ m / n.succ]
-[1+ m].div 0 = 0
↑m.div -[1+ n] = -int.of_nat (m / n.succ)
↑m.div ↑n = int.of_nat (m / n)

def int.mod (a a_1 : ℤ) :

Equations

-[1+ m].mod n = int.sub_nat_nat n.nat_abs (m % n.nat_abs).succ
↑m.mod n = ↑(m % n.nat_abs)

def int.fdiv (a a_1 : ℤ) :

Equations

-[1+ m].fdiv -[1+ n] = int.of_nat (m.succ / n.succ)
-[1+ m].fdiv ↑(n + 1) = -[1+ m / n.succ]
-[1+ m].fdiv 0 = 0
↑(m + 1).fdiv -[1+ n] = -[1+ m / n.succ]
↑(n.succ).fdiv ↑n_1 = int.of_nat (n.succ / n_1)
0.fdiv -[1+ a] = 0
0.fdiv (int.of_nat a) = 0

def int.fmod (a a_1 : ℤ) :

Equations

-[1+ m].fmod -[1+ n] = -int.of_nat (m.succ % n.succ)
-[1+ m].fmod ↑n = int.sub_nat_nat n (m % n).succ
↑(m + 1).fmod -[1+ n] = int.sub_nat_nat (m % n.succ) n
↑(n.succ).fmod ↑n_1 = int.of_nat (n.succ % n_1)
0.fmod -[1+ a] = 0
0.fmod (int.of_nat a) = 0

def int.quot (a a_1 : ℤ) :

Equations

-[1+ m].quot -[1+ n] = int.of_nat (m.succ / n.succ)
-[1+ m].quot (int.of_nat n) = -int.of_nat (m.succ / n)
(int.of_nat m).quot -[1+ n] = -int.of_nat (m / n.succ)
(int.of_nat m).quot (int.of_nat n) = int.of_nat (m / n)

def int.rem (a a_1 : ℤ) :

Equations

-[1+ m].rem -[1+ n] = -int.of_nat (m.succ % n.succ)
-[1+ m].rem (int.of_nat n) = -int.of_nat (m.succ % n)
(int.of_nat m).rem -[1+ n] = int.of_nat (m % n.succ)
(int.of_nat m).rem (int.of_nat n) = int.of_nat (m % n)

@[instance]

def int.has_div :

has_div ℤ

Equations

int.has_div = {div := int.div}

@[instance]

def int.has_mod :

has_mod ℤ

Equations

int.has_mod = {mod := int.mod}

def int.gcd (m n : ℤ) :

Equations

m.gcd n = m.nat_abs.gcd n.nat_abs

theorem int.add_comm (a b : ℤ) :

a + b = b + a

theorem int.add_zero (a : ℤ) :

a + 0 = a

theorem int.zero_add (a : ℤ) :

0 + a = a

theorem int.sub_nat_nat_sub {m n : ℕ} (h : m ≥ n) (k : ℕ) :

int.sub_nat_nat (m - n) k = int.sub_nat_nat m (k + n)

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

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)

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)

theorem int.add_assoc_aux2 (m n k : ℕ) :

-[1+ m] + -[1+ n] + int.of_nat k = -[1+ m] + (-[1+ n] + int.of_nat k)

theorem int.add_assoc (a b c : ℤ) :

a + b + c = a + (b + c)

theorem int.sub_nat_self (n : ℕ) :

int.sub_nat_nat n n = 0

theorem int.add_left_neg (a : ℤ) :

-a + a = 0

theorem int.add_right_neg (a : ℤ) :

a + -a = 0

theorem int.mul_comm (a b : ℤ) :

a * b = b * a

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)

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)

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)

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)

theorem int.mul_assoc (a b c : ℤ) :

(a * b) * c = a * b * c

theorem int.mul_zero (a : ℤ) :

a * 0 = 0

theorem int.zero_mul (a : ℤ) :

0 * a = 0

theorem int.neg_of_nat_eq_sub_nat_nat_zero (n : ℕ) :

int.neg_of_nat n = int.sub_nat_nat 0 n

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)

theorem int.neg_of_nat_add (m n : ℕ) :

int.neg_of_nat m + int.neg_of_nat n = int.neg_of_nat (m + n)

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)

theorem int.distrib_left (a b c : ℤ) :

a * (b + c) = a * b + a * c

theorem int.distrib_right (a b c : ℤ) :

(a + b) * c = a * c + b * c

theorem int.zero_ne_one :

0 ≠ 1

theorem int.of_nat_sub {n m : ℕ} (h : m ≤ n) :

int.of_nat (n - m) = int.of_nat n - int.of_nat m

theorem int.add_left_comm (a b c : ℤ) :

a + (b + c) = b + (a + c)

theorem int.add_left_cancel {a b c : ℤ} (h : a + b = a + c) :

b = c

theorem int.neg_add {a b : ℤ} :

-(a + b) = -a + -b

theorem int.neg_succ_of_nat_coe' (n : ℕ) :

-[1+ n] = -↑n - 1

theorem int.coe_nat_sub {n m : ℕ} (a : n ≤ m) :

↑(m - n) = ↑m - ↑n

theorem int.sub_nat_nat_eq_coe {m n : ℕ} :

int.sub_nat_nat m n = ↑m - ↑n

def int.to_nat (a : ℤ) :

Equations

-[1+ n].to_nat = 0
↑n.to_nat = n

theorem int.to_nat_sub (m n : ℕ) :

(↑m - ↑n).to_nat = m - n

def int.nat_mod (m n : ℤ) :

Equations

m.nat_mod n = (m % n).to_nat

theorem int.one_mul (a : ℤ) :

1 * a = a

theorem int.mul_one (a : ℤ) :

a * 1 = a

theorem int.neg_eq_neg_one_mul (a : ℤ) :

-a = (-1) * a