mathlib docs: core.init.data.int.basic

source

@[instance]

def int.decidable_eq :

decidable_eq ℤ

source

inductive int :

Type

of_nat : ℕ → ℤ
neg_succ_of_nat : ℕ → ℤ

source

@[instance]

def int.has_coe :

has_coe ℕ ℤ

Equations

int.has_coe = {coe := int.of_nat}

source

def int.repr :

ℤ → string

Equations

-[1+ n].repr = "-" ++ repr n.succ
(int.of_nat n).repr = repr n

source

@[instance]

def int.has_repr :

has_repr ℤ

Equations

int.has_repr = {repr := int.repr}

source

@[instance]

def int.has_to_string :

has_to_string ℤ

Equations

int.has_to_string = {to_string := int.repr}

source

theorem int.coe_nat_eq (n : ℕ) :

↑n = int.of_nat n

source

def int.zero :

ℤ

Equations

int.zero = int.of_nat 0

source

def int.one :

ℤ

Equations

int.one = int.of_nat 1

source

@[instance]

def int.has_zero :

has_zero ℤ

Equations

int.has_zero = {zero := int.zero}

source

@[instance]

def int.has_one :

has_one ℤ

Equations

int.has_one = {one := int.one}

source

theorem int.of_nat_zero :

int.of_nat 0 = 0

source

theorem int.of_nat_one :

int.of_nat 1 = 1

source

def int.neg_of_nat :

ℕ → ℤ

Equations

int.neg_of_nat m.succ = -[1+ m]
int.neg_of_nat 0 = 0

source

def int.sub_nat_nat :

ℕ → ℕ → ℤ

Equations

int.sub_nat_nat m n = int.sub_nat_nat._match_1 m n (n - m)
int.sub_nat_nat._match_1 m n k.succ = -[1+ k]
int.sub_nat_nat._match_1 m n 0 = int.of_nat (m - n)

source

def int.neg :

ℤ → ℤ

Equations

-[1+ n].neg = ↑(n.succ)
(int.of_nat n).neg = int.neg_of_nat n

source

def int.add :

ℤ → ℤ → ℤ

Equations

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

source

def int.mul :

ℤ → ℤ → ℤ

Equations

-[1+ m].mul -[1+ n] = int.of_nat (m.succ * n.succ)
-[1+ m].mul (int.of_nat n) = int.neg_of_nat (m.succ * n)
(int.of_nat m).mul -[1+ n] = int.neg_of_nat (m * n.succ)
(int.of_nat m).mul (int.of_nat n) = int.of_nat (m * n)

source

@[instance]

def int.has_neg :

has_neg ℤ

Equations

int.has_neg = {neg := int.neg}

source

@[instance]

def int.has_add :

has_add ℤ

Equations

int.has_add = {add := int.add}

source

@[instance]

def int.has_mul :

has_mul ℤ

Equations

int.has_mul = {mul := int.mul}

source

def int.sub :

ℤ → ℤ → ℤ

Equations

int.sub = λ (m n : ℤ), m + -n

source

@[instance]

def int.has_sub :

has_sub ℤ

Equations

int.has_sub = {sub := int.sub}

source

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

@[simp]

theorem int.coe_nat_add (m n : ℕ) :

↑(m + n) = ↑m + ↑n

source

@[simp]

theorem int.coe_nat_mul (m n : ℕ) :

↑(m * n) = ↑m * ↑n

source

@[simp]

theorem int.coe_nat_zero :

↑0 = 0

source

@[simp]

theorem int.coe_nat_one :

↑1 = 1

source

@[simp]

theorem int.coe_nat_succ (n : ℕ) :

↑(n.succ) = ↑n + 1

source

theorem int.coe_nat_add_out (m n : ℕ) :

↑m + ↑n = ↑m + ↑n

source

theorem int.coe_nat_mul_out (m n : ℕ) :

↑m * ↑n = ↑(m * n)

source

theorem int.coe_nat_add_one_out (n : ℕ) :

↑n + 1 = ↑(n.succ)

source

theorem int.coe_nat_inj {m n : ℕ} :

↑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

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)

source

theorem int.neg_neg (a : ℤ) :

--a = a

source

theorem int.neg_inj {a b : ℤ} :

-a = -b → a = b

source

theorem int.sub_eq_add_neg {a b : ℤ} :

a - b = a + -b

source

theorem int.sub_nat_nat_elim (m n : ℕ) (P : ℕ → ℕ → ℤ → Prop) :

(∀ (i n : ℕ), P (n + i) n (int.of_nat i)) → (∀ (i m : ℕ), P m (m + i + 1) -[1+ i]) → P m n (int.sub_nat_nat m n)

source

@[simp]

def int.nat_abs :

ℤ → ℕ

Equations

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

source

@[simp]

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 : ℤ} :

a ≠ 0 → a.nat_abs > 0

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

source

def int.sign :

ℤ → ℤ

Equations

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

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

source

def int.div :

ℤ → ℤ → ℤ

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)

source

def int.mod :

ℤ → ℤ → ℤ

Equations

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

source

def int.fdiv :

ℤ → ℤ → ℤ

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

source

def int.fmod :

ℤ → ℤ → ℤ

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

source

def int.quot :

ℤ → ℤ → ℤ

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)

source

def int.rem :

ℤ → ℤ → ℤ

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)

source

@[instance]

def int.has_div :

has_div ℤ

Equations

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

source

@[instance]

def int.has_mod :

has_mod ℤ

Equations

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

source

def int.gcd :

ℤ → ℤ → ℕ

Equations

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

source

theorem int.add_comm (a b : ℤ) :

a + b = b + a

source

theorem int.add_zero (a : ℤ) :

a + 0 = a

source

theorem int.zero_add (a : ℤ) :

0 + a = a

source

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

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

source

theorem int.add_left_neg (a : ℤ) :

-a + a = 0

source

theorem int.add_right_neg (a : ℤ) :

a + -a = 0

source

theorem int.mul_comm (a b : ℤ) :

a * b = b * a

source

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

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

source

theorem int.mul_zero (a : ℤ) :

a * 0 = 0

source

theorem int.zero_mul (a : ℤ) :

0 * a = 0

source

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

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

source

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

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

source

theorem int.zero_ne_one :

0 ≠ 1

source

theorem int.of_nat_sub {n m : ℕ} :

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

source

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

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

source

theorem int.add_left_cancel {a b c : ℤ} :

a + b = a + c → b = c

source

theorem int.neg_add {a b : ℤ} :

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

source

theorem int.neg_succ_of_nat_coe' (n : ℕ) :

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

source

theorem int.coe_nat_sub {n m : ℕ} :

n ≤ m → ↑(m - n) = ↑m - ↑n

source

theorem int.sub_nat_nat_eq_coe {m n : ℕ} :

int.sub_nat_nat m n = ↑m - ↑n

source

def int.to_nat :

ℤ → ℕ

Equations

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

source

theorem int.to_nat_sub (m n : ℕ) :

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

source

def int.nat_mod :

ℤ → ℤ → ℕ

Equations

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

source

theorem int.one_mul (a : ℤ) :

1 * a = a

source

theorem int.mul_one (a : ℤ) :

a * 1 = a

source

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

mathlib documentation

core.init.data.int.basic

General documentation

Additional documentation

Library

mathlib documentation

core.​init.​data.​int.​basic

General documentation

Additional documentation

Library

core.init.data.int.basic