Basic operations on the integers

This file builds on Data.Int.Init by adding basic lemmas on integers depending on Mathlib definitions.

instance Int.instNontrivial : Nontrivial ℤ

@[simp]

theorem Int.ofNat_injective : Function.Injective ofNat

theorem Int.strongRec_of_ge {m n : ℤ} {P : ℤ → Sort u_1} {lt : (n : ℤ) → n < m → P n} {ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n} (hn : m ≤ n) : Int.strongRec lt ge n = ge n hn fun (k : ℤ) (x : k < n) => Int.strongRec lt ge k

nat abs

theorem Int.natAbs_surjective : Function.Surjective natAbs

theorem Int.pow_right_injective {a : ℤ} (h : 1 < a.natAbs) : Function.Injective fun (x : ℕ) => a ^ x

dvd

theorem Int.ofNat_dvd_natCast {x y : ℕ} : OfNat.ofNat x ∣ ↑y ↔ OfNat.ofNat x ∣ y

theorem Int.natCast_dvd_ofNat {x y : ℕ} : ↑x ∣ OfNat.ofNat y ↔ x ∣ OfNat.ofNat y

theorem Int.natCast_dvd {n : ℤ} {m : ℕ} : ↑m ∣ n ↔ m ∣ n.natAbs

theorem Int.dvd_natCast {m : ℤ} {n : ℕ} : m ∣ ↑n ↔ m.natAbs ∣ n

theorem Int.eq_zero_of_dvd_of_nonneg_of_lt {m n : ℤ} (hm : 0 ≤ m) (hmn : m < n) (hnm : n ∣ m) : m = 0

theorem Int.eq_of_mod_eq_of_natAbs_sub_lt_natAbs {a b c : ℤ} (h1 : a % b = c) (h2 : (a - c).natAbs < b.natAbs) : a = c

If two integers are congruent to a sufficiently large modulus, they are equal.

theorem Int.natAbs_le_of_dvd_ne_zero {m n : ℤ} (hmn : m ∣ n) (hn : n ≠ 0) : m.natAbs ≤ n.natAbs

theorem Int.gcd_emod (m n : ℤ) : (m % n).gcd n = m.gcd n