Basic operations on the integers

This file contains:

• instances on ℤ. The stronger one is Int.linearOrderedCommRing.
• some basic lemmas about integers

ink

instance Int.instNontrivialInt : Nontrivial ℤ

Equations

• Int.instNontrivialInt = Int.instNontrivialInt.proof_1

ink

instance Int.instCommRingInt : CommRing ℤ

Equations

• Int.instCommRingInt = CommRing.mk Int.mul_comm

ink

@[simp]

theorem Int.cast_id {n : ℤ} : ↑n = n

ink

@[simp]

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

ink

theorem Int.cast_Nat_cast {R : Type u_1} {n : ℕ} [inst : AddGroupWithOne R] : ↑↑n = ↑n

ink

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

ink

@[simp]

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

ink

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

ink

@[simp]

theorem coe_nat_zsmul {G : Type u_1} [inst : SubNegMonoid G] (a : G) (n : ℕ) : ↑n • a = n • a

ink

@[simp]

theorem zpow_coe_nat {G : Type u_1} [inst : 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.

ink

instance Int.instAddCommMonoidInt : AddCommMonoid ℤ

Equations

• Int.instAddCommMonoidInt = inferInstance

ink

instance Int.instAddMonoidInt : AddMonoid ℤ

Equations

• Int.instAddMonoidInt = inferInstance

ink

instance Int.instMonoidInt : Monoid ℤ

Equations

• Int.instMonoidInt = inferInstance

ink

instance Int.instCommMonoidInt : CommMonoid ℤ

Equations

• Int.instCommMonoidInt = inferInstance

ink

instance Int.instCommSemigroupInt : CommSemigroup ℤ

Equations

• Int.instCommSemigroupInt = inferInstance

ink

instance Int.instSemigroupInt : Semigroup ℤ

Equations

• Int.instSemigroupInt = inferInstance

ink

instance Int.instAddCommGroupInt : AddCommGroup ℤ

Equations

• Int.instAddCommGroupInt = inferInstance

ink

instance Int.instAddGroupInt : AddGroup ℤ

Equations

• Int.instAddGroupInt = inferInstance

ink

instance Int.instAddCommSemigroupInt : AddCommSemigroup ℤ

Equations

• Int.instAddCommSemigroupInt = inferInstance

ink

instance Int.instAddSemigroupInt : AddSemigroup ℤ

Equations

• Int.instAddSemigroupInt = inferInstance

ink

instance Int.instCommSemiringInt : CommSemiring ℤ

Equations

• Int.instCommSemiringInt = inferInstance

ink

instance Int.instSemiringInt : Semiring ℤ

Equations

• Int.instSemiringInt = inferInstance

ink

instance Int.instRingInt : Ring ℤ

Equations

• Int.instRingInt = inferInstance

ink

instance Int.instDistribInt : Distrib ℤ

Equations

• Int.instDistribInt = inferInstance

ink

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

ink

theorem Int.coe_nat_strictMono : StrictMono fun x => ↑x

ink

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

ink

@[simp]

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

ink

@[simp]

theorem Int.sign_negSucc (n : ℕ) : Int.sign (Int.negSucc n) = -1

succ and pred

ink

def Int.succ (a : ℤ) : ℤ

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

Equations

• Int.succ a = a + 1

ink

def Int.pred (a : ℤ) : ℤ

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

Equations

• Int.pred a = a - 1

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

/

ink

@[simp]

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

ink

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

ink

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

mod

ink

@[simp]

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

properties of / and %

ink

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

toNat

ink

@[simp]

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

ink

@[simp]

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