Basic operations on the integers

This file contains some basic lemmas about integers.

See note [foundational algebra order theory].

TODO

Split this file into:

• Data.Int.Init (or maybe Data.Int.Std?) for lemmas that could go to Std
• Data.Int.Basic for the lemmas that require mathlib definitions

theorem Int.one_pos : 0 < 1

theorem Int.one_nonneg : 0 ≤ 1

theorem Int.zero_le_ofNat (n : ℕ) : 0 ≤ Int.ofNat n

instance Int.instNontrivial : Nontrivial ℤ

Equations

• Int.instNontrivial = ⋯

@[simp]

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

@[deprecated Int.ofNat_eq_natCast]

theorem Int.natCast_eq_ofNat (n : ℕ) : ↑n = Int.ofNat n

theorem Int.natCast_inj {m : ℕ} {n : ℕ} : ↑m = ↑n ↔ m = n

@[simp]

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

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

theorem Int.natCast_eq_zero {n : ℕ} : ↑n = 0 ↔ n = 0

theorem Int.natCast_ne_zero {n : ℕ} : ↑n ≠ 0 ↔ n ≠ 0

theorem Int.natCast_ne_zero_iff_pos {n : ℕ} : ↑n ≠ 0 ↔ 0 < n

theorem Int.natCast_nonneg (n : ℕ) : 0 ≤ ↑n

@[simp]

theorem Int.sign_natCast_add_one (n : ℕ) : (↑n + 1).sign = 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

• a.succ = a + 1

def Int.pred (a : ℤ) : ℤ

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

Equations

• a.pred = a - 1

theorem Int.natCast_succ (n : ℕ) : ↑n.succ = (↑n).succ

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

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

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

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

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

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

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

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

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

theorem Int.natCast_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_ofNat' (n : ℕ) : (Int.ofNat n).natAbs = n

theorem Int.natAbs_add_of_nonneg {a : ℤ} {b : ℤ} : 0 ≤ a → 0 ≤ b → (a + b).natAbs = a.natAbs + b.natAbs

theorem Int.natAbs_add_of_nonpos {a : ℤ} {b : ℤ} (ha : a ≤ 0) (hb : b ≤ 0) : (a + b).natAbs = a.natAbs + b.natAbs

theorem Int.natAbs_surjective : Function.Surjective Int.natAbs

@[deprecated Int.natAbs_ne_zero]

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

theorem Int.natAbs_sq (x : ℤ) : ↑x.natAbs ^ 2 = x ^ 2

theorem Int.natAbs_pow_two (x : ℤ) : ↑x.natAbs ^ 2 = x ^ 2

Alias of Int.natAbs_sq.

/

@[simp]

theorem Int.natCast_div (m : ℕ) (n : ℕ) : ↑(m / n) = ↑m / ↑n

theorem Int.natCast_ediv (m : ℕ) (n : ℕ) : ↑(m / n) = (↑m).ediv ↑n

theorem Int.ediv_of_neg_of_pos {a : ℤ} {b : ℤ} (Ha : a < 0) (Hb : 0 < b) : a.ediv b = -((-a - 1) / b + 1)

mod

@[simp]

theorem Int.natCast_mod (m : ℕ) (n : ℕ) : ↑(m % n) = ↑m % ↑n

properties of / and %

theorem Int.sign_natCast_of_ne_zero {n : ℕ} (hn : n ≠ 0) : (↑n).sign = 1

toNat

@[simp]

theorem Int.toNat_natCast (n : ℕ) : (↑n).toNat = n

@[simp]

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

@[simp]

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

@[deprecated Int.ofNat_eq_natCast]

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

Alias of Int.ofNat_eq_natCast.

@[deprecated Int.natCast_inj]

theorem Int.cast_eq_cast_iff_Nat {m : ℕ} {n : ℕ} : ↑m = ↑n ↔ m = n

Alias of Int.natCast_inj.

@[deprecated Int.natCast_sub]

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

Alias of Int.natCast_sub.

@[deprecated Int.natCast_nonneg]

theorem Int.coe_nat_nonneg (n : ℕ) : 0 ≤ ↑n

Alias of Int.natCast_nonneg.

@[deprecated Int.sign_natCast_add_one]

theorem Int.sign_coe_add_one (n : ℕ) : (↑n + 1).sign = 1

Alias of Int.sign_natCast_add_one.

@[deprecated Int.natCast_succ]

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

Alias of Int.natCast_succ.

@[deprecated Int.succ_neg_natCast_succ]

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

Alias of Int.succ_neg_natCast_succ.

@[deprecated Int.natCast_pred_of_pos]

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

Alias of Int.natCast_pred_of_pos.

@[deprecated Int.natCast_div]

theorem Int.coe_nat_div (m : ℕ) (n : ℕ) : ↑(m / n) = ↑m / ↑n

Alias of Int.natCast_div.

@[deprecated Int.natCast_ediv]

theorem Int.coe_nat_ediv (m : ℕ) (n : ℕ) : ↑(m / n) = (↑m).ediv ↑n

Alias of Int.natCast_ediv.

@[deprecated Int.sign_natCast_of_ne_zero]

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

Alias of Int.sign_natCast_of_ne_zero.

@[deprecated Int.toNat_natCast]

theorem Int.toNat_coe_nat (n : ℕ) : (↑n).toNat = n

Alias of Int.toNat_natCast.

@[deprecated Int.toNat_natCast_add_one]

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

Alias of Int.toNat_natCast_add_one.