Mathlib.Data.Int.Basic

Int.instNontrivial instance

: Nontrivial ℤ

Full source

instance instNontrivial : Nontrivial ℤ := ⟨⟨0, 1, Int.zero_ne_one⟩⟩

Nontriviality of the Integers

Informal description

The integers $\mathbb{Z}$ form a nontrivial type, meaning they contain at least two distinct elements.

Int.ofNat_injective theorem

: Function.Injective ofNat

Full source

@[simp] lemma ofNat_injective : Function.Injective ofNat := @Int.ofNat.inj

Injectivity of Natural Number Embedding into Integers

Informal description

The canonical embedding of natural numbers into integers, denoted by `ofNat`, is injective. That is, for any natural numbers $n$ and $m$, if $\text{ofNat}(n) = \text{ofNat}(m)$, then $n = m$.

Int.inductionOn'_add_one theorem

(hz : b ≤ z) : (z + 1).inductionOn' b H0 Hs Hp = Hs z hz (z.inductionOn' b H0 Hs Hp)

Full source

lemma inductionOn'_add_one (hz : b ≤ z) :
    (z + 1).inductionOn' b H0 Hs Hp = Hs z hz (z.inductionOn' b H0 Hs Hp) := by
  apply cast_eq_iff_heq.mpr
  lift z - b to ℕ using Int.sub_nonneg.mpr hz with zb hzb
  rw [show z + 1 - b = zb + 1 by omega]
  have : b + zb = z := by omega
  subst this
  convert cast_heq _ _
  rw [Int.inductionOn', cast_eq_iff_heq, ← hzb]

Induction Step for Integers with Base $b$ at $z + 1$

Informal description

For any integer $z$ and base integer $b$ such that $b \leq z$, the induction step at $z + 1$ with base $b$, zero case $H_0$, successor case $H_s$, and predecessor case $H_p$ is equal to applying the successor case $H_s$ to $z$, the proof $hz$ that $b \leq z$, and the induction result at $z$.

Int.strongRec_of_ge theorem

: ∀ hn : m ≤ n, m.strongRec lt ge n = ge n hn fun k _ ↦ m.strongRec lt ge k

Full source

lemma strongRec_of_ge :
    ∀ hn : m ≤ n, m.strongRec lt ge n = ge n hn fun k _ ↦ m.strongRec lt ge k := by
  refine m.strongRec (fun n hnm hmn ↦ (Int.not_lt.mpr hmn hnm).elim) (fun n _ ih hn ↦ ?_) n
  rw [Int.strongRec, dif_neg (Int.not_lt.mpr hn)]
  congr; revert ih
  refine n.inductionOn' m (fun _ ↦ ?_) (fun k hmk ih' ih ↦ ?_) (fun k hkm ih' _ ↦ ?_) <;> ext l hl
  · rw [inductionOn'_self, strongRec_of_lt hl]
  · rw [inductionOn'_add_one hmk]; split_ifs with hlm
    · rw [strongRec_of_lt hlm]
    · rw [ih' fun l hl ↦ ih l (Int.lt_trans hl k.lt_succ), ih _ hl]
  · rw [inductionOn'_sub_one hkm, ih']
    exact fun l hlk hml ↦ (Int.not_lt.mpr hkm <| Int.lt_of_le_of_lt hml hlk).elim

Strong Recursion Evaluation for Integers with $m \leq n$

Informal description

For any integers $m$ and $n$ such that $m \leq n$, the strong recursion function `m.strongRec` with cases `lt` and `ge` evaluated at $n$ equals the `ge` case applied to $n$, the proof `hn` that $m \leq n$, and the function that applies `m.strongRec` to any integer $k$ less than $n$.

Int.natAbs_surjective theorem

: natAbs.Surjective

Full source

lemma natAbs_surjective : natAbs.Surjective := fun n => ⟨n, natAbs_natCast n⟩

Surjectivity of the Natural Absolute Value Function on Integers

Informal description

The function $\operatorname{natAbs} : \mathbb{Z} \to \mathbb{N}$, which maps an integer to its absolute value as a natural number, is surjective. That is, for every natural number $n \in \mathbb{N}$, there exists an integer $z \in \mathbb{Z}$ such that $\operatorname{natAbs}(z) = n$.

Int.pow_right_injective theorem

(h : 1 < a.natAbs) : ((a ^ ·) : ℕ → ℤ).Injective

Full source

lemma pow_right_injective (h : 1 < a.natAbs) : ((a ^ ·) : ℕ → ℤ).Injective := by
  refine (?_ : (natAbsnatAbs ∘ (a ^ · : ℕ → ℤ)).Injective).of_comp
  convert Nat.pow_right_injective h using 2
  rw [Function.comp_apply, natAbs_pow]

Injectivity of Integer Power Function for $|a| > 1$

Informal description

For any integer $a$ with $|\operatorname{natAbs}(a)| > 1$, the power function $f(n) = a^n$ is injective on natural numbers. That is, for any natural numbers $m$ and $n$, if $a^m = a^n$, then $m = n$.

Int.natCast_dvd_natCast theorem

{m n : ℕ} : (↑m : ℤ) ∣ ↑n ↔ m ∣ n

Full source

@[norm_cast] lemma natCast_dvd_natCast {m n : ℕ} : (↑m : ℤ) ∣ ↑n(↑m : ℤ) ∣ ↑n ↔ m ∣ n where
  mp := by
    rintro ⟨a, h⟩
    obtain rfl | hm := m.eq_zero_or_pos
    · simpa using h
    have ha : 0 ≤ a := Int.not_lt.1 fun ha ↦ by
      simpa [← h, Int.not_lt.2 (Int.natCast_nonneg _)]
        using Int.mul_neg_of_pos_of_neg (natCast_pos.2 hm) ha
    lift a to ℕ using ha
    norm_cast at h
    exact ⟨a, h⟩
  mpr := by rintro ⟨a, rfl⟩; simp [Int.dvd_mul_right]

Divisibility Correspondence Between Natural Numbers and Integers

Informal description

For any natural numbers $m$ and $n$, the integer $m$ divides the integer $n$ if and only if the natural number $m$ divides the natural number $n$.

Int.ofNat_dvd_natCast theorem

{x y : ℕ} : (ofNat(x) : ℤ) ∣ (y : ℤ) ↔ OfNat.ofNat x ∣ y

Full source

@[norm_cast] theorem ofNat_dvd_natCast {x y : ℕ} : (ofNat(x) : ℤ) ∣ (y : ℤ)(ofNat(x) : ℤ) ∣ (y : ℤ) ↔ OfNat.ofNat x ∣ y :=
  natCast_dvd_natCast

Divisibility Correspondence Between Natural Numbers and Integers via OfNat

Informal description

For any natural numbers $x$ and $y$, the integer $x$ divides the integer $y$ if and only if the natural number $x$ divides the natural number $y$.

Int.natCast_dvd_ofNat theorem

{x y : ℕ} : (x : ℤ) ∣ (ofNat(y) : ℤ) ↔ x ∣ OfNat.ofNat y

Full source

@[norm_cast] theorem natCast_dvd_ofNat {x y : ℕ} : (x : ℤ) ∣ (ofNat(y) : ℤ)(x : ℤ) ∣ (ofNat(y) : ℤ) ↔ x ∣ OfNat.ofNat y :=
  natCast_dvd_natCast

Divisibility Correspondence Between Natural Numbers and Integers via OfNat

Informal description

For any natural numbers $x$ and $y$, the integer $x$ divides the integer $y$ if and only if the natural number $x$ divides the natural number $y$.

Int.natCast_dvd theorem

{m : ℕ} : (m : ℤ) ∣ n ↔ m ∣ n.natAbs

Full source

lemma natCast_dvd {m : ℕ} : (m : ℤ) ∣ n(m : ℤ) ∣ n ↔ m ∣ n.natAbs := by
  obtain hn | hn := natAbs_eq n <;> rw [hn] <;> simp [← natCast_dvd_natCast, Int.dvd_neg]

Divisibility of Integer by Natural Number via Absolute Value

Informal description

For any natural number $m$ and integer $n$, the integer $m$ divides $n$ if and only if $m$ divides the absolute value of $n$ as a natural number, i.e., $m \mid n \leftrightarrow m \mid |n|$.

Int.dvd_natCast theorem

{n : ℕ} : m ∣ (n : ℤ) ↔ m.natAbs ∣ n

Full source

lemma dvd_natCast {n : ℕ} : m ∣ (n : ℤ)m ∣ (n : ℤ) ↔ m.natAbs ∣ n := by
  obtain hn | hn := natAbs_eq m <;> rw [hn] <;> simp [← natCast_dvd_natCast, Int.neg_dvd]

Divisibility of Natural Cast to Integers via Absolute Value

Informal description

For any integer $m$ and natural number $n$, the integer $m$ divides the integer $n$ if and only if the absolute value of $m$ (as a natural number) divides $n$.

Int.natAbs_le_of_dvd_ne_zero theorem

(hmn : m ∣ n) (hn : n ≠ 0) : natAbs m ≤ natAbs n

Full source

lemma natAbs_le_of_dvd_ne_zero (hmn : m ∣ n) (hn : n ≠ 0) : natAbs m ≤ natAbs n :=
  not_lt.mp (mt (eq_zero_of_dvd_of_natAbs_lt_natAbs hmn) hn)

Natural Absolute Value Inequality for Nonzero Divisors: $m \mid n \land n \neq 0 \implies |m|_{\mathbb{N}} \leq |n|_{\mathbb{N}}$

Informal description

For any integers $m$ and $n$, if $m$ divides $n$ and $n$ is nonzero, then the natural absolute value of $m$ is less than or equal to the natural absolute value of $n$, i.e., $m \mid n \land n \neq 0 \implies |m|_{\mathbb{N}} \leq |n|_{\mathbb{N}}$.