# Documentation

Mathlib.Data.Int.Basic

# Basic operations on the integers #

This file contains:

• instances on ℤ. The stronger one is Int.linearOrderedCommRing.
• some basic lemmas about integers
Equations
Equations
@[simp]
theorem Int.cast_id {n : } :
n = n
@[simp]
theorem Int.ofNat_eq_cast {n : } :
= n
theorem Int.cast_Nat_cast {R : Type u_1} {n : } [inst : ] :
n = n
theorem Int.cast_eq_cast_iff_Nat (m : ) (n : ) :
m = n m = n
@[simp]
theorem Int.natAbs_cast (n : ) :
= n
theorem Int.coe_nat_sub {n : } {m : } :
n m↑(m - n) = m - n
@[simp]
theorem coe_nat_zsmul {G : Type u_1} [inst : ] (a : G) (n : ) :
n a = n a
@[simp]
theorem zpow_coe_nat {G : Type u_1} [inst : ] (a : G) (n : ) :
a ^ n = a ^ n

### Extra instances to short-circuit type class resolution #

These also prevent non-computable instances like Int.normedCommRing being used to construct these instances non-computably.

Equations
Equations
Equations
Equations
Equations
Equations
instance Int.instRingInt :
Equations
Equations
theorem Int.coe_nat_inj' {m : } {n : } :
m = n m = n
theorem Int.coe_nat_nonneg (n : ) :
0 n
@[simp]
theorem Int.sign_coe_add_one (n : ) :
Int.sign (n + 1) = 1
@[simp]
theorem Int.sign_negSucc (n : ) :
= -1

### succ and pred #

def Int.succ (a : ) :

Immediate successor of an integer: succ n = n + 1

Equations
def Int.pred (a : ) :

Immediate predecessor of an integer: pred n = n - 1

Equations
theorem Int.pred_succ (a : ) :
Int.pred () = a
theorem Int.succ_pred (a : ) :
Int.succ () = a
theorem Int.neg_succ (a : ) :
theorem Int.neg_pred (a : ) :
theorem Int.pred_nat_succ (n : ) :
Int.pred ↑() = n
theorem Int.neg_nat_succ (n : ) :
-↑() = Int.pred (-n)
theorem Int.succ_neg_nat_succ (n : ) :
Int.succ (-↑()) = -n
theorem Int.coe_pred_of_pos {n : } (h : 0 < n) :
↑(n - 1) = n - 1
theorem Int.induction_on {p : } (i : ) (hz : p 0) (hp : (i : ) → p ip (i + 1)) (hn : (i : ) → p (-i)p (-i - 1)) :
p i

### /#

@[simp]
theorem Int.coe_nat_div (m : ) (n : ) :
↑(m / n) = m / n
theorem Int.coe_nat_ediv (m : ) (n : ) :
↑(m / n) = Int.ediv m n
theorem Int.ediv_of_neg_of_pos {a : } {b : } (Ha : a < 0) (Hb : 0 < b) :
Int.ediv a b = -((-a - 1) / b + 1)

### mod #

@[simp]
theorem Int.coe_nat_mod (m : ) (n : ) :
↑(m % n) = m % n

### properties of / and %#

theorem Int.sign_coe_nat_of_nonzero {n : } (hn : n 0) :
Int.sign n = 1

### toNat #

@[simp]
theorem Int.toNat_coe_nat (n : ) :
= n
@[simp]
theorem Int.toNat_coe_nat_add_one {n : } :
Int.toNat (n + 1) = n + 1