Basic operations on the integers

This file contains some basic lemmas about integers.

instance Int.instNontrivialInt : Nontrivial ℤ

Equations

• Int.instNontrivialInt = (_ : Nontrivial ℤ)

@[simp]

theorem Int.ofNat_eq_cast {n : ℕ} : Int.ofNat n = ↑n

theorem Int.cast_eq_cast_iff_Nat (m : ℕ) (n : ℕ) : ↑m = ↑n ↔ m = n

@[simp]

theorem Int.natAbs_cast (n : ℕ) : Int.natAbs ↑n = n

theorem Int.coe_nat_sub {n : ℕ} {m : ℕ} : n ≤ m → ↑(m - n) = ↑m - ↑n

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

theorem Int.two_mul (n : ℤ) : 2 * n = n + n

@[deprecated]

theorem Int.ofNat_bit0 (n : ℕ) : ↑(bit0 n) = bit0 ↑n

@[deprecated]

theorem Int.ofNat_bit1 (n : ℕ) : ↑(bit1 n) = bit1 ↑n

succ and pred

def Int.succ (a : ℤ) : ℤ

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

Equations

• Int.succ a = a + 1

def Int.pred (a : ℤ) : ℤ

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

Equations

• Int.pred a = a - 1

theorem Int.nat_succ_eq_int_succ (n : ℕ) : ↑(Nat.succ n) = Int.succ ↑n

theorem Int.pred_succ (a : ℤ) : Int.pred (Int.succ a) = a

theorem Int.succ_pred (a : ℤ) : Int.succ (Int.pred a) = a

theorem Int.neg_succ (a : ℤ) : -Int.succ a = Int.pred (-a)

theorem Int.succ_neg_succ (a : ℤ) : Int.succ (-Int.succ a) = -a

theorem Int.neg_pred (a : ℤ) : -Int.pred a = Int.succ (-a)

theorem Int.pred_neg_pred (a : ℤ) : Int.pred (-Int.pred a) = -a

theorem Int.pred_nat_succ (n : ℕ) : Int.pred ↑(Nat.succ n) = ↑n

theorem Int.neg_nat_succ (n : ℕ) : -↑(Nat.succ n) = Int.pred (-↑n)

theorem Int.succ_neg_nat_succ (n : ℕ) : Int.succ (-↑(Nat.succ n)) = -↑n

theorem Int.coe_pred_of_pos {n : ℕ} (h : 0 < n) : ↑(n - 1) = ↑n - 1

theorem Int.induction_on {p : ℤ → Prop} (i : ℤ) (hz : p 0) (hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)) (hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)) : p i

nat abs

theorem Int.natAbs_surjective : Function.Surjective Int.natAbs

@[deprecated Int.natAbs_ne_zero]

theorem Int.natAbs_ne_zero_of_ne_zero {a : ℤ} : a ≠ 0 → Int.natAbs a ≠ 0

/

@[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 : ℕ) : Int.toNat ↑n = n

@[simp]

theorem Int.toNat_coe_nat_add_one {n : ℕ} : Int.toNat (↑n + 1) = n + 1

@[simp]

theorem Int.pow_eq (m : ℤ) (n : ℕ) : Int.pow m n = m ^ n