Documentation

Mathlib.Data.Int.Defs

Basic operations on the integers #

This file contains some basic lemmas about integers.

source
instance Int.instNontrivialInt :
Nontrivial ℤ
Equations
source
@[simp]
theorem Int.ofNat_eq_natCast {n : ℕ} :
Int.ofNat n = ↑n
source
@[deprecated Int.ofNat_eq_natCast]
theorem Int.natCast_eq_ofNat (n : ℕ) :
↑n = Int.ofNat n
source
theorem Int.natCast_inj {m : ℕ} {n : ℕ} :
↑m = ↑n ↔ m = n
source
@[simp]
theorem Int.natAbs_cast (n : ℕ) :
Int.natAbs ↑n = n
source
theorem Int.natCast_sub {n : ℕ} {m : ℕ} :
n ≤ m → ↑(m - n) = ↑m - ↑n
source
theorem Int.natCast_nonneg (n : ℕ) :
0 ≤ ↑n
source
@[simp]
theorem Int.sign_natCast_add_one (n : ℕ) :
Int.sign (↑n + 1) = 1
source
theorem Int.two_mul (n : ℤ) :
2 * n = n + n
source
@[deprecated]
theorem Int.ofNat_bit0 (n : ℕ) :
↑(bit0 n) = bit0 ↑n
source
@[deprecated]
theorem Int.ofNat_bit1 (n : ℕ) :
↑(bit1 n) = bit1 ↑n

succ and pred #

source
def Int.succ (a : ℤ) :
ℤ

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

Equations
Instances For
    source
    def Int.pred (a : ℤ) :
    ℤ

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

    Equations
    Instances For
      source
      theorem Int.natCast_succ (n : ℕ) :
      ↑(Nat.succ n) = Int.succ ↑n
      source
      theorem Int.pred_succ (a : ℤ) :
      Int.pred (Int.succ a) = a
      source
      theorem Int.succ_pred (a : ℤ) :
      Int.succ (Int.pred a) = a
      source
      theorem Int.neg_succ (a : ℤ) :
      -Int.succ a = Int.pred (-a)
      source
      theorem Int.succ_neg_succ (a : ℤ) :
      Int.succ (-Int.succ a) = -a
      source
      theorem Int.neg_pred (a : ℤ) :
      -Int.pred a = Int.succ (-a)
      source
      theorem Int.pred_neg_pred (a : ℤ) :
      Int.pred (-Int.pred a) = -a
      source
      theorem Int.pred_nat_succ (n : ℕ) :
      Int.pred ↑(Nat.succ n) = ↑n
      source
      theorem Int.neg_nat_succ (n : ℕ) :
      -↑(Nat.succ n) = Int.pred (-↑n)
      source
      theorem Int.succ_neg_natCast_succ (n : ℕ) :
      Int.succ (-↑(Nat.succ n)) = -↑n
      source
      theorem Int.natCast_pred_of_pos {n : ℕ} (h : 0 < n) :
      ↑(n - 1) = ↑n - 1
      source
      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 #

      source
      theorem Int.natAbs_surjective :
      Function.Surjective Int.natAbs
      source
      @[deprecated Int.natAbs_ne_zero]
      theorem Int.natAbs_ne_zero_of_ne_zero {a : ℤ} :
      a ≠ 0 → Int.natAbs a ≠ 0

      / #

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

      mod #

      source
      @[simp]
      theorem Int.natCast_mod (m : ℕ) (n : ℕ) :
      ↑(m % n) = ↑m % ↑n

      properties of / and % #

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

      toNat #

      source
      @[simp]
      theorem Int.toNat_natCast (n : ℕ) :
      Int.toNat ↑n = n
      source
      @[simp]
      theorem Int.toNat_natCast_add_one {n : ℕ} :
      Int.toNat (↑n + 1) = n + 1
      source
      @[simp]
      theorem Int.pow_eq (m : ℤ) (n : ℕ) :
      Int.pow m n = m ^ n
      source
      @[deprecated Int.ofNat_eq_natCast]
      theorem Int.ofNat_eq_cast {n : ℕ} :
      Int.ofNat n = ↑n

      Alias of Int.ofNat_eq_natCast.

      source
      @[deprecated Int.natCast_inj]
      theorem Int.cast_eq_cast_iff_Nat {m : ℕ} {n : ℕ} :
      ↑m = ↑n ↔ m = n

      Alias of Int.natCast_inj.

      source
      @[deprecated Int.natCast_sub]
      theorem Int.coe_nat_sub {n : ℕ} {m : ℕ} :
      n ≤ m → ↑(m - n) = ↑m - ↑n

      Alias of Int.natCast_sub.

      source
      @[deprecated Int.natCast_nonneg]
      theorem Int.coe_nat_nonneg (n : ℕ) :
      0 ≤ ↑n

      Alias of Int.natCast_nonneg.

      source
      @[deprecated Int.sign_natCast_add_one]
      theorem Int.sign_coe_add_one (n : ℕ) :
      Int.sign (↑n + 1) = 1

      Alias of Int.sign_natCast_add_one.

      source
      @[deprecated Int.natCast_succ]
      theorem Int.nat_succ_eq_int_succ (n : ℕ) :
      ↑(Nat.succ n) = Int.succ ↑n

      Alias of Int.natCast_succ.

      source
      @[deprecated Int.succ_neg_natCast_succ]
      theorem Int.succ_neg_nat_succ (n : ℕ) :
      Int.succ (-↑(Nat.succ n)) = -↑n

      Alias of Int.succ_neg_natCast_succ.

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

      source
      @[deprecated Int.natCast_div]
      theorem Int.coe_nat_div (m : ℕ) (n : ℕ) :
      ↑(m / n) = ↑m / ↑n

      Alias of Int.natCast_div.

      source
      @[deprecated Int.natCast_ediv]
      theorem Int.coe_nat_ediv (m : ℕ) (n : ℕ) :
      ↑(m / n) = Int.ediv ↑m ↑n

      Alias of Int.natCast_ediv.

      source
      @[deprecated Int.sign_natCast_of_ne_zero]
      theorem Int.sign_coe_nat_of_nonzero {n : ℕ} (hn : n ≠ 0) :
      Int.sign ↑n = 1

      Alias of Int.sign_natCast_of_ne_zero.

      source
      @[deprecated Int.toNat_natCast]
      theorem Int.toNat_coe_nat (n : ℕ) :
      Int.toNat ↑n = n

      Alias of Int.toNat_natCast.

      source
      @[deprecated Int.toNat_natCast_add_one]
      theorem Int.toNat_coe_nat_add_one {n : ℕ} :
      Int.toNat (↑n + 1) = n + 1

      Alias of Int.toNat_natCast_add_one.