Documentation

Mathlib.Data.Int.Basic

Basic operations on the integers #

This file contains:

source
instance Int.instNontrivialInt :
Nontrivial ℤ
source
instance Int.instCommRingInt :
CommRing ℤ
source
@[simp]
theorem Int.cast_id {n : ℤ} :
↑n = n
source
@[simp]
theorem Int.cast_mul {α : Type u_1} [NonAssocRing α] (m : ℤ) (n : ℤ) :
↑(m * n) = ↑m * ↑n
source
@[simp]
theorem Int.ofNat_eq_cast {n : ℕ} :
Int.ofNat n = ↑n
source
theorem Int.cast_Nat_cast {R : Type u_1} {n : ℕ} [AddGroupWithOne R] :
↑↑n = ↑n
source
theorem Int.cast_eq_cast_iff_Nat (m : ℕ) (n : ℕ) :
↑m = ↑n ↔ m = n
source
@[simp]
theorem Int.natAbs_cast (n : ℕ) :
Int.natAbs ↑n = n
source
theorem Int.coe_nat_sub {n : ℕ} {m : ℕ} :
n ≤ m → ↑(m - n) = ↑m - ↑n
source
@[simp]
theorem coe_nat_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) (n : ℕ) :
↑n • a = n • a
source
@[simp]
theorem zpow_coe_nat {G : Type u_1} [DivInvMonoid G] (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.

source
instance Int.instAddCommMonoidInt :
AddCommMonoid ℤ
source
instance Int.instAddMonoidInt :
AddMonoid ℤ
source
instance Int.instMonoidInt :
Monoid ℤ
source
instance Int.instCommMonoidInt :
CommMonoid ℤ
source
instance Int.instCommSemigroupInt :
CommSemigroup ℤ
source
instance Int.instSemigroupInt :
Semigroup ℤ
source
instance Int.instAddCommGroupInt :
AddCommGroup ℤ
source
instance Int.instAddGroupInt :
AddGroup ℤ
source
instance Int.instAddCommSemigroupInt :
AddCommSemigroup ℤ
source
instance Int.instAddSemigroupInt :
AddSemigroup ℤ
source
instance Int.instCommSemiringInt :
CommSemiring ℤ
source
instance Int.instSemiringInt :
Semiring ℤ
source
instance Int.instRingInt :
Ring ℤ
source
instance Int.instDistribInt :
Distrib ℤ
source
theorem Int.coe_nat_inj' {m : ℕ} {n : ℕ} :
↑m = ↑n ↔ m = n
source
theorem Int.coe_nat_strictMono :
StrictMono fun x => ↑x
source
theorem Int.coe_nat_nonneg (n : ℕ) :
0 ≤ ↑n
source
@[simp]
theorem Int.sign_coe_add_one (n : ℕ) :
Int.sign (↑n + 1) = 1
source
@[simp]
theorem Int.sign_negSucc (n : ℕ) :
Int.sign (Int.negSucc n) = -1

succ and pred #

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

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

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

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

    Instances For
      source
      theorem Int.nat_succ_eq_int_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_nat_succ (n : ℕ) :
      Int.succ (-↑(Nat.succ n)) = -↑n
      source
      theorem Int.coe_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.coe_nat_div (m : ℕ) (n : ℕ) :
      ↑(m / n) = ↑m / ↑n
      source
      theorem Int.coe_nat_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.coe_nat_mod (m : ℕ) (n : ℕ) :
      ↑(m % n) = ↑m % ↑n

      properties of / and % #

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

      toNat #

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