Init.Data.Int.Lemmas

Int.subNatNat_of_sub_eq_zero theorem

{m n : Nat} (h : n - m = 0) : subNatNat m n = ↑(m - n)

Full source

theorem subNatNat_of_sub_eq_zero {m n : Nat} (h : n - m = 0) : subNatNat m n = ↑(m - n) := by
  rw [subNatNat, h, ofNat_eq_coe]

`subNatNat` Equals Canonical Image When Natural Subtraction is Zero

Informal description

For any natural numbers $m$ and $n$, if $n - m = 0$, then the integer subtraction of $m$ from $n$ via `subNatNat` equals the canonical image of the natural number subtraction $m - n$ in the integers.

Int.subNatNat_of_sub_eq_succ theorem

{m n k : Nat} (h : n - m = succ k) : subNatNat m n = -[k+1]

Full source

theorem subNatNat_of_sub_eq_succ {m n k : Nat} (h : n - m = succ k) : subNatNat m n = -[k+1] := by
  rw [subNatNat, h]

`subNatNat` Result When Truncated Subtraction Yields Successor

Informal description

For any natural numbers $m$, $n$, and $k$, if the truncated subtraction $n - m$ equals the successor of $k$ (i.e., $n - m = k + 1$), then the result of the `subNatNat` operation on $m$ and $n$ is equal to the negative integer $- (k + 1)$ (denoted as `-[k+1]`).

Int.neg_zero theorem

: -(0 : Int) = 0

Full source

@[simp] protected theorem neg_zero : -(0:Int) = 0 := rfl

Negation of Zero Equals Zero in Integers

Informal description

The negation of the integer zero is equal to zero, i.e., $-0 = 0$.

Int.ofNat_add theorem

(n m : Nat) : (↑(n + m) : Int) = n + m

Full source

@[norm_cast] theorem ofNat_add (n m : Nat) : (↑(n + m) : Int) = n + m := rfl

Canonical Homomorphism Preserves Addition: $(n + m : \mathbb{Z}) = n + m$

Informal description

For any natural numbers $n$ and $m$, the canonical image of their sum in the integers equals their sum as integers, i.e., $(n + m : \mathbb{Z}) = n + m$.

Int.ofNat_mul theorem

(n m : Nat) : (↑(n * m) : Int) = n * m

Full source

@[norm_cast] theorem ofNat_mul (n m : Nat) : (↑(n * m) : Int) = n * m := rfl

Canonical Homomorphism Preserves Multiplication: $(n \cdot m : \mathbb{Z}) = n \cdot m$

Informal description

For any natural numbers $n$ and $m$, the canonical image of their product in the integers equals their product as integers, i.e., $(n \cdot m : \mathbb{Z}) = n \cdot m$.

Int.ofNat_succ theorem

(n : Nat) : (succ n : Int) = n + 1

Full source

@[norm_cast] theorem ofNat_succ (n : Nat) : (succ n : Int) = n + 1 := rfl

Canonical Image of Successor in Integers: $(n + 1 : \mathbb{Z}) = n + 1$

Informal description

For any natural number $n$, the canonical image of the successor of $n$ in the integers is equal to $n + 1$, i.e., $(n + 1 : \mathbb{Z}) = n + 1$.

Int.neg_ofNat_zero theorem

: -((0 : Nat) : Int) = 0

Full source

theorem neg_ofNat_zero : -((0 : Nat) : Int) = 0 := rfl

Negation of Zero in Integers: $-0 = 0$

Informal description

The negation of the integer obtained by casting the natural number $0$ is equal to $0$, i.e., $-((0 : \mathbb{N}) : \mathbb{Z}) = 0$.

Int.neg_ofNat_succ theorem

(n : Nat) : -(succ n : Int) = -[n+1]

Full source

theorem neg_ofNat_succ (n : Nat) : -(succ n : Int) = -[n+1] := rfl

Negation of Successor Natural Number in Integers: $-(\text{succ } n) = -[n+1]$

Informal description

For any natural number $n$, the negation of the integer successor of $n$ (i.e., $-((n + 1) : \mathbb{Z})$) is equal to the negative integer $-[n+1]$.

Int.neg_negSucc theorem

(n : Nat) : -(-[n+1]) = succ n

Full source

theorem neg_negSucc (n : Nat) : -(-[n+1]) = succ n := rfl

Double Negation of Negative Successor Equals Successor: $-(-[n+1]) = n + 1$

Informal description

For any natural number $n$, the negation of the negative successor $-(-[n+1])$ is equal to the successor $\text{succ } n$.

Int.negOfNat_eq theorem

: negOfNat n = -ofNat n

Full source

theorem negOfNat_eq : negOfNat n = -ofNat n := rfl

Negation of Natural Number as Integer Equals Negation of Canonical Embedding

Informal description

For any natural number $n$, the negation of the natural number $n$ as an integer, denoted $\text{negOfNat}(n)$, is equal to the negation of the canonical embedding of $n$ into the integers, i.e., $\text{negOfNat}(n) = -(\text{ofNat}(n))$.

Int.add_def theorem

{a b : Int} : Int.add a b = a + b

Full source

@[simp] theorem add_def {a b : Int} : Int.add a b = a + b := rfl

Integer Addition Definition: $\text{Int.add}(a, b) = a + b$

Informal description

For any integers $a$ and $b$, the addition operation `Int.add a b` is equal to the sum $a + b$.

Int.mul_def theorem

{a b : Int} : Int.mul a b = a * b

Full source

@[simp] theorem mul_def {a b : Int} : Int.mul a b = a * b := rfl

Integer Multiplication Definition: $\text{Int.mul}(a, b) = a * b$

Informal description

For any integers $a$ and $b$, the multiplication operation `Int.mul a b` is equal to the product $a * b$.

Int.ofNat_add_ofNat theorem

(m n : Nat) : (↑m + ↑n : Int) = ↑(m + n)

Full source

@[local simp] theorem ofNat_add_ofNat (m n : Nat) : (↑m + ↑n : Int) = ↑(m + n) := rfl

Canonical Integer Addition Preserves Natural Number Addition

Informal description

For any natural numbers $m$ and $n$, the sum of their canonical integer representations equals the canonical integer representation of their sum. In symbols: $$ m + n = (m + n) $$ where the left-hand side addition is performed in the integers and the right-hand side addition is performed in the natural numbers.

Int.ofNat_add_negSucc theorem

(m n : Nat) : ↑m + -[n+1] = subNatNat m (succ n)

Full source

@[local simp] theorem ofNat_add_negSucc (m n : Nat) : ↑m + -[n+1] = subNatNat m (succ n) := rfl

Integer Addition: Canonical Natural Plus Negative Successor Equals `subNatNat`

Informal description

For any natural numbers $m$ and $n$, the sum of the canonical integer representation of $m$ and the negative successor of $n$ (i.e., $-n-1$) is equal to the result of the `subNatNat` function applied to $m$ and $n+1$. In symbols: $$ \text{Int.ofNat}(m) + (-[n+1]) = \text{subNatNat}(m, n+1) $$

Int.negSucc_add_ofNat theorem

(m n : Nat) : -[m+1] + ↑n = subNatNat n (succ m)

Full source

@[local simp] theorem negSucc_add_ofNat (m n : Nat) : -[m+1] + ↑n = subNatNat n (succ m) := rfl

Integer Addition: Negative Successor Plus Natural Equals `subNatNat`

Informal description

For any natural numbers $m$ and $n$, the sum of the negative successor $-m-1$ and the canonical integer representation of $n$ equals the result of the `subNatNat` function applied to $n$ and $m+1$. In symbols: $$ -[m+1] + n = \text{subNatNat}(n, m+1) $$

Int.negSucc_add_negSucc theorem

(m n : Nat) : -[m+1] + -[n+1] = -[succ (m + n)+1]

Full source

@[local simp] theorem negSucc_add_negSucc (m n : Nat) : -[m+1] + -[n+1] = -[succ (m + n) +1] := rfl

Sum of Negative Successors in Integers

Informal description

For any natural numbers $m$ and $n$, the sum of the negative successors $-m-1$ and $-n-1$ equals the negative successor of $(m + n + 1)$. In symbols: $$ -[m+1] + -[n+1] = -[(m + n) + 2] $$

Int.ofNat_mul_ofNat theorem

(m n : Nat) : (↑m * ↑n : Int) = ↑(m * n)

Full source

@[local simp] theorem ofNat_mul_ofNat (m n : Nat) : (↑m * ↑n : Int) = ↑(m * n) := rfl

Integer Multiplication Preserves Natural Number Multiplication

Informal description

For any natural numbers $m$ and $n$, the product of their canonical integer representations equals the canonical integer representation of their product, i.e., $m \cdot n = (m \cdot n)$ where the left side is multiplication in $\mathbb{Z}$ and the right side is multiplication in $\mathbb{N}$.

Int.ofNat_inj theorem

: ((m : Nat) : Int) = (n : Nat) ↔ m = n

Full source

@[norm_cast] theorem ofNat_inj : ((m : Nat) : Int) = (n : Nat) ↔ m = n := ⟨ofNat.inj, congrArg _⟩

Injectivity of the Natural Number to Integer Embedding

Informal description

For any natural numbers $m$ and $n$, the canonical embedding of $m$ into the integers equals the canonical embedding of $n$ into the integers if and only if $m = n$. In other words, the canonical map $\mathbb{N} \to \mathbb{Z}$ is injective.

Int.ofNat_eq_zero theorem

: ((n : Nat) : Int) = 0 ↔ n = 0

Full source

theorem ofNat_eq_zero : ((n : Nat) : Int) = 0 ↔ n = 0 := ofNat_inj

Embedding of Natural Number into Integers is Zero iff $n = 0$

Informal description

For any natural number $n$, the canonical embedding of $n$ into the integers equals zero if and only if $n = 0$.

Int.ofNat_ne_zero theorem

: ((n : Nat) : Int) ≠ 0 ↔ n ≠ 0

Full source

theorem ofNat_ne_zero : ((n : Nat) : Int) ≠ 0((n : Nat) : Int) ≠ 0 ↔ n ≠ 0 := not_congr ofNat_eq_zero

Nonzero Natural Number Embedding in Integers

Informal description

For any natural number $n$, the canonical embedding of $n$ into the integers is not equal to zero if and only if $n$ is not equal to zero, i.e., $(n : \mathbb{Z}) \neq 0 \leftrightarrow n \neq 0$.

Int.negSucc_inj theorem

: negSucc m = negSucc n ↔ m = n

Full source

theorem negSucc_inj : negSuccnegSucc m = negSucc n ↔ m = n := ⟨negSucc.inj, fun H => by simp [H]⟩

Injective Property of Negative Successor Integers: $- [m+1] = - [n+1] \leftrightarrow m = n$

Informal description

For any natural numbers $m$ and $n$, the negative successor integers $- [m+1]$ and $- [n+1]$ are equal if and only if $m = n$.

Int.negSucc_eq theorem

(n : Nat) : -[n+1] = -((n : Int) + 1)

Full source

theorem negSucc_eq (n : Nat) : -[n+1] = -((n : Int) + 1) := rfl

Negative Successor Integer Equality: $- [n+1] = -((n : \mathbb{Z}) + 1)$

Informal description

For any natural number $n$, the negative successor integer $- [n+1]$ is equal to the negation of the integer obtained by adding 1 to the natural number $n$, i.e., $- [n+1] = -((n : \mathbb{Z}) + 1)$.

Int.negSucc_coe theorem

(n : Nat) : -[n+1] = -↑(n + 1)

Full source

@[deprecated negSucc_eq (since := "2025-03-11")]
theorem negSucc_coe (n : Nat) : -[n+1] = -↑(n + 1) := rfl

Negative Successor Integer as Negation of Canonical Image: $- [n+1] = - (n + 1)$

Informal description

For any natural number $n$, the negative successor integer $- [n+1]$ is equal to the negation of the canonical image of $n + 1$ in the integers, i.e., $- [n+1] = - (n + 1)$.

Int.negSucc_ne_zero theorem

(n : Nat) : -[n+1] ≠ 0

Full source

@[simp] theorem negSucc_ne_zero (n : Nat) : -[n+1]-[n+1] ≠ 0 := nofun

Nonzero Property of Negative Successor Integers: $- [n+1] \neq 0$

Informal description

For any natural number $n$, the negative successor integer $- [n+1]$ is not equal to zero.

Int.zero_ne_negSucc theorem

(n : Nat) : 0 ≠ -[n+1]

Full source

@[simp] theorem zero_ne_negSucc (n : Nat) : 0 ≠ -[n+1] := nofun

Nonzero Property of Negative Successor Integers: $0 \neq - [n+1]$

Informal description

For any natural number $n$, the integer $0$ is not equal to $- [n+1]$.

Int.cast_ofNat_Int theorem

: (Nat.cast (no_index (OfNat.ofNat n)) : Int) = OfNat.ofNat n

Full source

@[simp, norm_cast] theorem cast_ofNat_Int :
  (Nat.cast (no_index (OfNat.ofNat n)) : Int) = OfNat.ofNat n := rfl

Natural Number to Integer Cast Identity: $\text{Nat.cast}(n) = n$

Informal description

For any natural number $n$, the canonical homomorphism from natural numbers to integers maps the natural number $n$ to the integer $n$, i.e., $\text{Nat.cast}(n) = n$ in $\mathbb{Z}$.

Int.neg_neg theorem

: ∀ a : Int, -(-a) = a

Full source

@[simp] protected theorem neg_neg : ∀ a : Int, -(-a) = a
  | 0      => rfl
  | succ _ => rfl
  | -[_+1] => rfl

Double Negation Identity for Integers: $-(-a) = a$

Informal description

For any integer $a$, the negation of the negation of $a$ equals $a$, i.e., $-(-a) = a$.

Int.neg_inj theorem

{a b : Int} : -a = -b ↔ a = b

Full source

@[simp] protected theorem neg_inj {a b : Int} : -a = -b ↔ a = b :=
  ⟨fun h => by rw [← Int.neg_neg a, ← Int.neg_neg b, h], congrArg _⟩

Negation is Injective on Integers: $-a = -b \leftrightarrow a = b$

Informal description

For any integers $a$ and $b$, the negation of $a$ equals the negation of $b$ if and only if $a$ equals $b$, i.e., $-a = -b \leftrightarrow a = b$.

Int.neg_eq_zero theorem

: -a = 0 ↔ a = 0

Full source

@[simp] protected theorem neg_eq_zero : -a = 0 ↔ a = 0 := Int.neg_inj (b := 0)

Negation Equals Zero iff Original Equals Zero: $-a = 0 \leftrightarrow a = 0$

Informal description

For any integer $a$, the negation of $a$ equals zero if and only if $a$ equals zero, i.e., $-a = 0 \leftrightarrow a = 0$.

Int.neg_ne_zero theorem

: -a ≠ 0 ↔ a ≠ 0

Full source

protected theorem neg_ne_zero : -a ≠ 0-a ≠ 0 ↔ a ≠ 0 := not_congr Int.neg_eq_zero

Negation Nonzero iff Original Nonzero: $-a \neq 0 \leftrightarrow a \neq 0$

Informal description

For any integer $a$, the negation of $a$ is not equal to zero if and only if $a$ itself is not equal to zero, i.e., $-a \neq 0 \leftrightarrow a \neq 0$.

Int.sub_eq_add_neg theorem

{a b : Int} : a - b = a + -b

Full source

protected theorem sub_eq_add_neg {a b : Int} : a - b = a + -b := rfl

Subtraction as Addition of Negative: $a - b = a + (-b)$

Informal description

For any integers $a$ and $b$, the subtraction $a - b$ is equal to the addition $a + (-b)$.

Int.add_neg_eq_sub theorem

{a b : Int} : a + -b = a - b

Full source

protected theorem add_neg_eq_sub {a b : Int} : a + -b = a - b := rfl

Integer Addition of Negative Equals Subtraction: $a + (-b) = a - b$

Informal description

For any integers $a$ and $b$, the sum $a + (-b)$ is equal to the difference $a - b$.

Int.add_neg_one theorem

(i : Int) : i + -1 = i - 1

Full source

theorem add_neg_one (i : Int) : i + -1 = i - 1 := rfl

Integer Addition of Negative One Equals Subtraction of One: $i + (-1) = i - 1$

Informal description

For any integer $i$, the sum of $i$ and $-1$ is equal to the difference of $i$ and $1$, i.e., $i + (-1) = i - 1$.

Int.subNatNat_elim theorem

 (m n : Nat) (motive : Nat → Nat → Int → Prop) (hp : ∀ i n, motive (n + i) n i)
  (hn : ∀ i m, motive m (m + i + 1) -[i+1]) : motive m n (subNatNat m n)

Full source

@[elab_as_elim]
theorem subNatNat_elim (m n : Nat) (motive : Nat → Nat → Int → Prop)
    (hp : ∀ i n, motive (n + i) n i)
    (hn : ∀ i m, motive m (m + i + 1) -[i+1]) :
    motive m n (subNatNat m n) := by
  unfold subNatNat
  match h : n - m with
  | 0 =>
    have ⟨k, h⟩ := Nat.le.dest (Nat.le_of_sub_eq_zero h)
    rw [h.symm, Nat.add_sub_cancel_left]; apply hp
  | succ k =>
    rw [Nat.sub_eq_iff_eq_add (Nat.le_of_lt (Nat.lt_of_sub_eq_succ h))] at h
    rw [h, Nat.add_comm]; apply hn

Elimination Principle for Integer Subtraction via Natural Numbers

Informal description

For any natural numbers $m$ and $n$, and a predicate $\text{motive}$ on triples of natural numbers and an integer, if: 1. For all $i$ and $n$, $\text{motive}(n + i, n, i)$ holds, and 2. For all $i$ and $m$, $\text{motive}(m, m + i + 1, -[i+1])$ holds, then $\text{motive}(m, n, \text{subNatNat}(m, n))$ holds. Here, $\text{subNatNat}(m, n)$ is the integer obtained by subtracting $n$ from $m$ (which may be negative if $n > m$), and $-[i+1]$ denotes the negative integer $-(i+1)$.

Int.subNatNat_add_left theorem

: subNatNat (m + n) m = n

Full source

theorem subNatNat_add_left : subNatNat (m + n) m = n := by
  unfold subNatNat
  rw [Nat.sub_eq_zero_of_le (Nat.le_add_right ..), Nat.add_sub_cancel_left, ofNat_eq_coe]

Left Addition Cancellation for subNatNat: $\text{subNatNat}(m + n, m) = n$

Informal description

For any natural numbers $m$ and $n$, the function $\text{subNatNat}$ satisfies $\text{subNatNat}(m + n, m) = n$.

Int.subNatNat_add_right theorem

: subNatNat m (m + n + 1) = negSucc n

Full source

theorem subNatNat_add_right : subNatNat m (m + n + 1) = negSucc n := by
  simp [subNatNat, Nat.add_assoc, Nat.add_sub_cancel_left]

$\text{subNatNat}(m, m + n + 1) = -(n + 1)$ for natural numbers $m, n$

Informal description

For any natural numbers $m$ and $n$, the function `subNatNat` satisfies the identity $\text{subNatNat}(m, m + n + 1) = \text{negSucc}(n)$, where $\text{negSucc}(n)$ represents the negative integer $-(n + 1)$.

Int.subNatNat_add_add theorem

(m n k : Nat) : subNatNat (m + k) (n + k) = subNatNat m n

Full source

theorem subNatNat_add_add (m n k : Nat) : subNatNat (m + k) (n + k) = subNatNat m n := by
  apply subNatNat_elim m n (fun m n i => subNatNat (m + k) (n + k) = i)
  focus
    intro i j
    rw [Nat.add_assoc, Nat.add_comm i k, ← Nat.add_assoc]
    exact subNatNat_add_left
  focus
    intro i j
    rw [Nat.add_assoc j i 1, Nat.add_comm j (i+1), Nat.add_assoc, Nat.add_comm (i+1) (j+k)]
    exact subNatNat_add_right

Translation Invariance of Integer Subtraction via Natural Numbers: $\text{subNatNat}(m + k, n + k) = \text{subNatNat}(m, n)$

Informal description

For any natural numbers $m$, $n$, and $k$, the integer subtraction operation $\text{subNatNat}$ satisfies $\text{subNatNat}(m + k, n + k) = \text{subNatNat}(m, n)$.

Int.subNatNat_of_le theorem

{m n : Nat} (h : n ≤ m) : subNatNat m n = ↑(m - n)

Full source

theorem subNatNat_of_le {m n : Nat} (h : n ≤ m) : subNatNat m n = ↑(m - n) :=
  subNatNat_of_sub_eq_zero (Nat.sub_eq_zero_of_le h)

Integer Subtraction via `subNatNat` Equals Natural Subtraction When $n \leq m$

Informal description

For any natural numbers $m$ and $n$ such that $n \leq m$, the integer subtraction operation `subNatNat` satisfies $\text{subNatNat}(m, n) = (m - n)$, where the right-hand side is the canonical image of the natural number subtraction in the integers.

Int.subNatNat_of_lt theorem

{m n : Nat} (h : m < n) : subNatNat m n = -[pred (n - m)+1]

Full source

theorem subNatNat_of_lt {m n : Nat} (h : m < n) : subNatNat m n = -[pred (n - m) +1] :=
  subNatNat_of_sub_eq_succ <| (Nat.succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)).symm

`subNatNat` Result for $m < n$: $\text{subNatNat}(m, n) = -(\mathrm{pred}(n - m) + 1)$

Informal description

For any natural numbers $m$ and $n$ such that $m < n$, the integer subtraction operation `subNatNat` satisfies $\text{subNatNat}(m, n) = -(\mathrm{pred}(n - m) + 1)$, where $\mathrm{pred}(k)$ denotes the predecessor of $k$ (i.e., $\max(k - 1, 0)$).

Int.subNat_eq_zero_iff theorem

{a b : Nat} : subNatNat a b = 0 ↔ a = b

Full source

@[simp] theorem subNat_eq_zero_iff {a b : Nat} : subNatNatsubNatNat a b = 0 ↔ a = b := by
  cases Nat.lt_or_ge a b with
  | inl h =>
    rw [subNatNat_of_lt h]
    simpa using ne_of_lt h
  | inr h =>
    rw [subNatNat_of_le h]
    norm_cast
    rw [Nat.sub_eq_iff_eq_add' h]
    simp

Zero Result of `subNatNat` Characterizes Equality of Natural Numbers

Informal description

For any natural numbers $a$ and $b$, the integer subtraction operation `subNatNat` yields zero if and only if $a = b$. That is, $\text{subNatNat}(a, b) = 0 \leftrightarrow a = b$.

Int.subNatNat_sub theorem

(h : n ≤ m) (k : Nat) : subNatNat (m - n) k = subNatNat m (k + n)

Full source

theorem subNatNat_sub (h : n ≤ m) (k : Nat) : subNatNat (m - n) k = subNatNat m (k + n) := by
  rwa [← subNatNat_add_add _ _ n, Nat.sub_add_cancel]

Subtraction-Translation Property of `subNatNat`: $\text{subNatNat}(m - n, k) = \text{subNatNat}(m, k + n)$ when $n \leq m$

Informal description

For any natural numbers $m$, $n$, and $k$ such that $n \leq m$, the integer subtraction operation $\text{subNatNat}$ satisfies $\text{subNatNat}(m - n, k) = \text{subNatNat}(m, k + n)$.

Int.subNatNat_add theorem

(m n k : Nat) : subNatNat (m + n) k = m + subNatNat n k

Full source

theorem subNatNat_add (m n k : Nat) : subNatNat (m + n) k = m + subNatNat n k := by
  cases n.lt_or_ge k with
  | inl h' =>
    simp [subNatNat_of_lt h', sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h')]
    conv => lhs; rw [← Nat.sub_add_cancel (Nat.le_of_lt h')]
    apply subNatNat_add_add
  | inr h' => simp [subNatNat_of_le h',
      subNatNat_of_le (Nat.le_trans h' (le_add_left ..)), Nat.add_sub_assoc h']

Additivity of `subNatNat` with respect to the first argument: $\text{subNatNat}(m + n, k) = m + \text{subNatNat}(n, k)$

Informal description

For any natural numbers $m$, $n$, and $k$, the integer subtraction operation $\text{subNatNat}$ satisfies $\text{subNatNat}(m + n, k) = m + \text{subNatNat}(n, k)$.

Int.subNatNat_add_negSucc theorem

(m n k : Nat) : subNatNat m n + -[k+1] = subNatNat m (n + succ k)

Full source

theorem subNatNat_add_negSucc (m n k : Nat) :
    subNatNat m n + -[k+1] = subNatNat m (n + succ k) := by
  have h := Nat.lt_or_ge m n
  cases h with
  | inr h' =>
    rw [subNatNat_of_le h']
    simp
    rw [subNatNat_sub h', Nat.add_comm]
  | inl h' =>
    have h₂ : m < n + succ k := Nat.lt_of_lt_of_le h' (le_add_right _ _)
    rw [subNatNat_of_lt h', subNatNat_of_lt h₂]
    simp only [pred_eq_sub_one, negSucc_add_negSucc, succ_eq_add_one, negSucc.injEq]
    rw [Nat.add_right_comm, sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h'), Nat.sub_sub,
      ← Nat.add_assoc, succ_sub_succ_eq_sub, Nat.add_comm n,Nat.add_sub_assoc (Nat.le_of_lt h'),
      Nat.add_comm]

Additivity of `subNatNat` with Negative Successor: $\text{subNatNat}(m, n) + -[k+1] = \text{subNatNat}(m, n + k + 1)$

Informal description

For any natural numbers $m$, $n$, and $k$, the sum of the integer subtraction operation $\text{subNatNat}(m, n)$ and the negative successor $-(\text{succ}(k))$ equals $\text{subNatNat}(m, n + \text{succ}(k))$.

Int.subNatNat_self theorem

: ∀ n, subNatNat n n = 0

Full source

theorem subNatNat_self : ∀ n, subNatNat n n = 0
  | 0      => rfl
  | succ m => by rw [subNatNat_of_sub_eq_zero (Nat.sub_self ..), Nat.sub_self, ofNat_zero]

`subNatNat` of a Natural Number with Itself Yields Zero

Informal description

For any natural number $n$, the integer subtraction operation `subNatNat` satisfies `subNatNat n n = 0`.

Int.add_comm theorem

: ∀ a b : Int, a + b = b + a

Full source

protected theorem add_comm : ∀ a b : Int, a + b = b + a
  | ofNat n, ofNat m => by simp [Nat.add_comm]
  | ofNat _, -[_+1]  => rfl
  | -[_+1],  ofNat _ => rfl
  | -[_+1],  -[_+1]  => by simp [Nat.add_comm]

Commutativity of Integer Addition: $a + b = b + a$

Informal description

For any integers $a$ and $b$, the sum $a + b$ is equal to $b + a$.

Int.instCommutativeHAdd instance

: Std.Commutative (α := Int) (· + ·)

Full source

instance : Std.Commutative (α := Int) (· + ·) := ⟨Int.add_comm⟩

Commutativity of Integer Addition

Informal description

The addition operation on integers is commutative.

Int.add_zero theorem

: ∀ a : Int, a + 0 = a

Full source

@[simp] protected theorem add_zero : ∀ a : Int, a + 0 = a
  | ofNat _ => rfl
  | -[_+1]  => rfl

Right Additive Identity for Integers

Informal description

For any integer $a$, the sum of $a$ and $0$ is equal to $a$, i.e., $a + 0 = a$.

Int.zero_add theorem

(a : Int) : 0 + a = a

Full source

@[simp] protected theorem zero_add (a : Int) : 0 + a = a := Int.add_comm .. ▸ a.add_zero

Left Additive Identity for Integers: $0 + a = a$

Informal description

For any integer $a$, the sum of $0$ and $a$ is equal to $a$, i.e., $0 + a = a$.

Int.instLawfulIdentityHAddOfNat instance

: Std.LawfulIdentity (α := Int) (· + ·) 0

Full source

instance : Std.LawfulIdentity (α := Int) (· + ·) 0 where
  left_id := Int.zero_add
  right_id := Int.add_zero

$0$ is the Additive Identity for Integers

Informal description

The integer $0$ is a lawful identity element for the addition operation on integers, meaning it satisfies both left and right identity laws: $0 + a = a$ and $a + 0 = a$ for any integer $a$.

Int.ofNat_add_negSucc_of_lt theorem

(h : m < n.succ) : ofNat m + -[n+1] = -[n - m+1]

Full source

theorem ofNat_add_negSucc_of_lt (h : m < n.succ) : ofNat m + -[n+1] = -[n - m+1] :=
  show subNatNat .. = _ by simp [succ_sub (le_of_lt_succ h), subNatNat]

Integer Addition Identity: $\text{ofNat}(m) + (-[n+1]) = -[(n - m) + 1]$ when $m < n + 1$

Informal description

For any natural numbers $m$ and $n$ such that $m < n + 1$, the sum of the integer representation of $m$ and the negative successor of $n$ equals the negative successor of $(n - m)$, i.e., $\text{ofNat}(m) + (-[n+1]) = -[(n - m) + 1]$.

Int.add_assoc theorem

: ∀ a b c : Int, a + b + c = a + (b + c)

Full source

protected theorem add_assoc : ∀ a b c : Int, a + b + c = a + (b + c)
  | (m:Nat), (n:Nat), _ => aux1 ..
  | Nat.cast m, b, Nat.cast k => by
    rw [Int.add_comm, ← aux1, Int.add_comm k, aux1, Int.add_comm b]
  | a, (n:Nat), (k:Nat) => by
    rw [Int.add_comm, Int.add_comm a, ← aux1, Int.add_comm a, Int.add_comm k]
  | -[_+1], -[_+1], (k:Nat) => aux2 ..
  | -[m+1], (n:Nat), -[k+1] => by
    rw [Int.add_comm, ← aux2, Int.add_comm n, ← aux2, Int.add_comm -[m+1]]
  | (m:Nat), -[n+1], -[k+1] => by
    rw [Int.add_comm, Int.add_comm m, Int.add_comm m, ← aux2, Int.add_comm -[k+1]]
  | -[m+1], -[n+1], -[k+1] => by
    simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]
where
  aux1 (m n : Nat) : ∀ c : Int, m + n + c = m + (n + c)
    | (k:Nat) => by simp [Nat.add_assoc]
    | -[k+1]  => by simp [subNatNat_add]
  aux2 (m n k : Nat) : -[m+1] + -[n+1] + k = -[m+1] + (-[n+1] + k) := by
    simp
    rw [Int.add_comm, subNatNat_add_negSucc]
    simp [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc]

Associativity of Integer Addition: $(a + b) + c = a + (b + c)$

Informal description

For any integers $a$, $b$, and $c$, the addition operation satisfies the associative property: $(a + b) + c = a + (b + c)$.

Int.instAssociativeHAdd instance

: Std.Associative (α := Int) (· + ·)

Full source

instance : Std.Associative (α := Int) (· + ·) := ⟨Int.add_assoc⟩

Associativity of Heterogeneous Addition on Integers

Informal description

The heterogeneous addition operation on integers is associative.

Int.add_left_comm theorem

(a b c : Int) : a + (b + c) = b + (a + c)

Full source

protected theorem add_left_comm (a b c : Int) : a + (b + c) = b + (a + c) := by
  rw [← Int.add_assoc, Int.add_comm a, Int.add_assoc]

Left-Commutativity of Integer Addition: $a + (b + c) = b + (a + c)$

Informal description

For any integers $a$, $b$, and $c$, the addition operation satisfies the left-commutative property: $a + (b + c) = b + (a + c)$.

Int.add_right_comm theorem

(a b c : Int) : a + b + c = a + c + b

Full source

protected theorem add_right_comm (a b c : Int) : a + b + c = a + c + b := by
  rw [Int.add_assoc, Int.add_comm b, ← Int.add_assoc]

Right Commutativity of Integer Addition: $a + b + c = a + c + b$

Informal description

For any integers $a$, $b$, and $c$, the sum $a + b + c$ is equal to $a + c + b$.

Int.add_left_neg theorem

: ∀ a : Int, -a + a = 0

Full source

protected theorem add_left_neg : ∀ a : Int, -a + a = 0
  | 0      => rfl
  | succ m => by simp [neg_ofNat_succ]
  | -[m+1] => by simp [neg_negSucc]

Additive Inverse Property for Integers: $-a + a = 0$

Informal description

For every integer $a$, the sum of $-a$ and $a$ equals zero, i.e., $-a + a = 0$.

Int.add_right_neg theorem

(a : Int) : a + -a = 0

Full source

protected theorem add_right_neg (a : Int) : a + -a = 0 := by
  rw [Int.add_comm, Int.add_left_neg]

Right Additive Inverse Property for Integers: $a + (-a) = 0$

Informal description

For every integer $a$, the sum of $a$ and its additive inverse $-a$ equals zero, i.e., $a + (-a) = 0$.

Int.neg_eq_of_add_eq_zero theorem

{a b : Int} (h : a + b = 0) : -a = b

Full source

protected theorem neg_eq_of_add_eq_zero {a b : Int} (h : a + b = 0) : -a = b := by
  rw [← Int.add_zero (-a), ← h, ← Int.add_assoc, Int.add_left_neg, Int.zero_add]

Negation from Sum Zero: $a + b = 0 \implies -a = b$

Informal description

For any integers $a$ and $b$, if $a + b = 0$, then $-a = b$.

Int.neg_eq_comm theorem

{a b : Int} : -a = b ↔ -b = a

Full source

protected theorem neg_eq_comm {a b : Int} : -a = b ↔ -b = a := by
  rw [eq_comm, Int.eq_neg_comm, eq_comm]

Negation Equality Commutation: $-a = b \leftrightarrow -b = a$

Informal description

For any integers $a$ and $b$, the negation of $a$ equals $b$ if and only if the negation of $b$ equals $a$, i.e., $-a = b \leftrightarrow -b = a$.

Int.neg_add_cancel_left theorem

(a b : Int) : -a + (a + b) = b

Full source

protected theorem neg_add_cancel_left (a b : Int) : -a + (a + b) = b := by
  rw [← Int.add_assoc, Int.add_left_neg, Int.zero_add]

Left Cancellation Property for Integer Addition: $-a + (a + b) = b$

Informal description

For any integers $a$ and $b$, the sum of $-a$ and $(a + b)$ equals $b$, i.e., $-a + (a + b) = b$.

Int.add_neg_cancel_left theorem

(a b : Int) : a + (-a + b) = b

Full source

protected theorem add_neg_cancel_left (a b : Int) : a + (-a + b) = b := by
  rw [← Int.add_assoc, Int.add_right_neg, Int.zero_add]

Left Cancellation of Negated Addition in Integers: $a + (-a + b) = b$

Informal description

For any integers $a$ and $b$, the sum of $a$ and $-a + b$ equals $b$, i.e., $a + (-a + b) = b$.

Int.add_neg_cancel_right theorem

(a b : Int) : a + b + -b = a

Full source

protected theorem add_neg_cancel_right (a b : Int) : a + b + -b = a := by
  rw [Int.add_assoc, Int.add_right_neg, Int.add_zero]

Right Additive Inverse Cancellation for Integers: $(a + b) + (-b) = a$

Informal description

For any integers $a$ and $b$, the sum of $a + b$ and $-b$ equals $a$, i.e., $(a + b) + (-b) = a$.

Int.neg_add_cancel_right theorem

(a b : Int) : a + -b + b = a

Full source

protected theorem neg_add_cancel_right (a b : Int) : a + -b + b = a := by
  rw [Int.add_assoc, Int.add_left_neg, Int.add_zero]

Right Cancellation of Additive Inverse in Integers: $(a + (-b)) + b = a$

Informal description

For any integers $a$ and $b$, the expression $(a + (-b)) + b$ simplifies to $a$.

Int.add_left_cancel theorem

{a b c : Int} (h : a + b = a + c) : b = c

Full source

protected theorem add_left_cancel {a b c : Int} (h : a + b = a + c) : b = c := by
  have h₁ : -a + (a + b) = -a + (a + c) := by rw [h]
  simp [← Int.add_assoc, Int.add_left_neg, Int.zero_add] at h₁; exact h₁

Left Cancellation Property for Integer Addition: $a + b = a + c \implies b = c$

Informal description

For any integers $a, b, c$, if $a + b = a + c$, then $b = c$.

Int.neg_add theorem

{a b : Int} : -(a + b) = -a + -b

Full source

protected theorem neg_add {a b : Int} : -(a + b) = -a + -b := by
  apply Int.add_left_cancel (a := a + b)
  rw [Int.add_right_neg, Int.add_comm a, ← Int.add_assoc, Int.add_assoc b,
    Int.add_right_neg, Int.add_zero, Int.add_right_neg]

Negation of Sum Equals Sum of Negations in Integers

Informal description

For any integers $a$ and $b$, the negation of their sum equals the sum of their negations, i.e., $-(a + b) = (-a) + (-b)$.

Int.wlog_sign theorem

{P : Int → Prop} (inv : ∀ i, P i ↔ P (-i)) (w : ∀ n : Nat, P n) (i : Int) : P i

Full source

/--
If a predicate on the integers is invariant under negation,
then it is sufficient to prove it for the nonnegative integers.
-/
theorem wlog_sign {P : Int → Prop} (inv : ∀ i, P i ↔ P (-i)) (w : ∀ n : Nat, P n) (i : Int) : P i := by
  cases i with
  | ofNat n => exact w n
  | negSucc n =>
    rw [negSucc_eq, ← inv, ← ofNat_succ]
    apply w

Reduction of Integer Predicate to Nonnegative Integers via Negation Invariance

Informal description

Let $P$ be a predicate on the integers such that for every integer $i$, $P(i)$ holds if and only if $P(-i)$ holds. If $P(n)$ holds for every natural number $n$, then $P(i)$ holds for every integer $i$.

Int.negSucc_sub_one theorem

(n : Nat) : -[n+1] - 1 = -[n + 1+1]

Full source

@[simp] theorem negSucc_sub_one (n : Nat) : -[n+1] - 1 = -[n + 1 +1] := rfl

Negative Successor Subtraction Identity: $- (n + 1) - 1 = - (n + 2)$

Informal description

For any natural number $n$, the integer $- (n + 1) - 1$ is equal to $- (n + 2)$.

Int.sub_self theorem

(a : Int) : a - a = 0

Full source

@[simp] protected theorem sub_self (a : Int) : a - a = 0 := by
  rw [Int.sub_eq_add_neg, Int.add_right_neg]

Self-Subtraction Property for Integers: $a - a = 0$

Informal description

For any integer $a$, the difference $a - a$ equals $0$.

Int.sub_zero theorem

(a : Int) : a - 0 = a

Full source

@[simp] protected theorem sub_zero (a : Int) : a - 0 = a := by simp [Int.sub_eq_add_neg]

Subtraction of Zero from an Integer: $a - 0 = a$

Informal description

For any integer $a$, the difference $a - 0$ equals $a$.

Int.zero_sub theorem

(a : Int) : 0 - a = -a

Full source

@[simp] protected theorem zero_sub (a : Int) : 0 - a = -a := by simp [Int.sub_eq_add_neg]

Subtraction from Zero: $0 - a = -a$

Informal description

For any integer $a$, the difference $0 - a$ equals $-a$.

Int.sub_eq_zero_of_eq theorem

{a b : Int} (h : a = b) : a - b = 0

Full source

protected theorem sub_eq_zero_of_eq {a b : Int} (h : a = b) : a - b = 0 := by
  rw [h, Int.sub_self]

Difference of Equal Integers is Zero: $a = b \Rightarrow a - b = 0$

Informal description

For any integers $a$ and $b$, if $a = b$, then $a - b = 0$.

Int.sub_eq_zero theorem

{a b : Int} : a - b = 0 ↔ a = b

Full source

protected theorem sub_eq_zero {a b : Int} : a - b = 0 ↔ a = b :=
  ⟨Int.eq_of_sub_eq_zero, Int.sub_eq_zero_of_eq⟩

Difference Equals Zero iff Integers Are Equal: $a - b = 0 \leftrightarrow a = b$

Informal description

For any integers $a$ and $b$, the difference $a - b$ equals zero if and only if $a = b$.

Int.sub_sub theorem

(a b c : Int) : a - b - c = a - (b + c)

Full source

protected theorem sub_sub (a b c : Int) : a - b - c = a - (b + c) := by
  simp [Int.sub_eq_add_neg, Int.add_assoc, Int.neg_add]

Integer Subtraction Associativity: $a - b - c = a - (b + c)$

Informal description

For any integers $a$, $b$, and $c$, the difference $a - b - c$ is equal to $a - (b + c)$.

Int.neg_sub theorem

(a b : Int) : -(a - b) = b - a

Full source

protected theorem neg_sub (a b : Int) : -(a - b) = b - a := by
  simp [Int.sub_eq_add_neg, Int.add_comm, Int.neg_add]

Negation of Integer Difference: $-(a - b) = b - a$

Informal description

For any integers $a$ and $b$, the negation of the difference $a - b$ equals the difference $b - a$, i.e., $-(a - b) = b - a$.

Int.sub_sub_self theorem

(a b : Int) : a - (a - b) = b

Full source

protected theorem sub_sub_self (a b : Int) : a - (a - b) = b := by
  simp [Int.sub_eq_add_neg, ← Int.add_assoc, Int.neg_add, Int.add_right_neg]

Integer Subtraction Identity: $a - (a - b) = b$

Informal description

For any integers $a$ and $b$, the expression $a - (a - b)$ simplifies to $b$.

Int.sub_neg theorem

(a b : Int) : a - -b = a + b

Full source

@[simp] protected theorem sub_neg (a b : Int) : a - -b = a + b := by simp [Int.sub_eq_add_neg]

Subtraction of Negative Integer: $a - (-b) = a + b$

Informal description

For any integers $a$ and $b$, the difference $a - (-b)$ is equal to the sum $a + b$.

Int.sub_add_cancel theorem

(a b : Int) : a - b + b = a

Full source

@[simp] protected theorem sub_add_cancel (a b : Int) : a - b + b = a :=
  Int.neg_add_cancel_right a b

Integer Subtraction-Add Cancellation: $(a - b) + b = a$

Informal description

For any integers $a$ and $b$, the expression $(a - b) + b$ equals $a$.

Int.add_sub_cancel theorem

(a b : Int) : a + b - b = a

Full source

@[simp] protected theorem add_sub_cancel (a b : Int) : a + b - b = a :=
  Int.add_neg_cancel_right a b

Right Cancellation of Addition and Subtraction for Integers: $(a + b) - b = a$

Informal description

For any integers $a$ and $b$, the expression $(a + b) - b$ equals $a$.

Int.add_sub_assoc theorem

(a b c : Int) : a + b - c = a + (b - c)

Full source

protected theorem add_sub_assoc (a b c : Int) : a + b - c = a + (b - c) := by
  rw [Int.sub_eq_add_neg, Int.add_assoc, Int.add_neg_eq_sub]

Associativity of Integer Addition and Subtraction: $(a + b) - c = a + (b - c)$

Informal description

For any integers $a$, $b$, and $c$, the expression $(a + b) - c$ is equal to $a + (b - c)$.

Int.ofNat_sub theorem

(h : m ≤ n) : ((n - m : Nat) : Int) = n - m

Full source

@[norm_cast] theorem ofNat_sub (h : m ≤ n) : ((n - m : Nat) : Int) = n - m := by
  match m with
  | 0 => rfl
  | succ m =>
    show ofNat (n - succ m) = subNatNat n (succ m)
    rw [subNatNat, Nat.sub_eq_zero_of_le h]

Canonical Map Preserves Subtraction of Natural Numbers under Truncated Condition

Informal description

For any natural numbers $m$ and $n$ such that $m \leq n$, the canonical map from natural numbers to integers satisfies $\text{cast}(n - m) = \text{cast}(n) - \text{cast}(m)$.

Int.negSucc_coe' theorem

(n : Nat) : -[n+1] = -↑n - 1

Full source

@[deprecated negSucc_eq (since := "2025-03-11")]
theorem negSucc_coe' (n : Nat) : -[n+1] = -↑n - 1 := by
  rw [Int.sub_eq_add_neg, ← Int.neg_add]; rfl

Negative Successor as Negative Cast Minus One: $- [n+1] = -n - 1$

Informal description

For any natural number $n$, the integer $- [n+1]$ (the negative successor of $n$) is equal to $-n - 1$, where $n$ is cast to an integer via the canonical embedding $\mathbb{N} \to \mathbb{Z}$.

Int.subNatNat_eq_coe theorem

{m n : Nat} : subNatNat m n = ↑m - ↑n

Full source

protected theorem subNatNat_eq_coe {m n : Nat} : subNatNat m n = ↑m - ↑n := by
  apply subNatNat_elim m n fun m n i => i = m - n
  · intros i n
    rw [Int.ofNat_add, Int.sub_eq_add_neg, Int.add_assoc, Int.add_left_comm,
      Int.add_right_neg, Int.add_zero]
  · intros i n
    simp only [negSucc_eq, ofNat_add, ofNat_one, Int.sub_eq_add_neg, Int.neg_add, ← Int.add_assoc]
    rw [Int.add_neg_eq_sub (a := n), ← ofNat_sub, Nat.sub_self, ofNat_zero, Int.zero_add]
    apply Nat.le_refl

Integer Subtraction via Natural Numbers Equals Canonical Difference

Informal description

For any natural numbers $m$ and $n$, the integer subtraction operation `subNatNat m n` equals the difference between the canonical images of $m$ and $n$ in the integers, i.e., $\text{subNatNat}(m, n) = m - n$.

Int.toNat_sub theorem

(m n : Nat) : toNat (m - n) = m - n

Full source

@[simp] theorem toNat_sub (m n : Nat) : toNat (m - n) = m - n := by
  rw [← Int.subNatNat_eq_coe]
  refine subNatNat_elim m n (fun m n i => toNat i = m - n) (fun i n => ?_) (fun i n => ?_)
  · exact (Nat.add_sub_cancel_left ..).symm
  · dsimp; rw [Nat.add_assoc, Nat.sub_eq_zero_of_le (Nat.le_add_right ..)]; rfl

Natural Number Truncated Subtraction via Integer Difference: $\text{toNat}(m - n) = m - n$

Informal description

For any natural numbers $m$ and $n$, the natural number obtained by applying the `toNat` function to the integer difference $m - n$ equals the truncated subtraction $m - n$ of the natural numbers.

Int.toNat_of_nonpos theorem

: ∀ {z : Int}, z ≤ 0 → z.toNat = 0

Full source

theorem toNat_of_nonpos : ∀ {z : Int}, z ≤ 0 → z.toNat = 0
  | 0, _ => rfl
  | -[_+1], _ => rfl

Nonpositive Integers Map to Zero under `toNat`

Informal description

For any integer $z$ such that $z \leq 0$, the natural number obtained by applying the `toNat` function to $z$ is equal to $0$.

Int.neg_ofNat_eq_negSucc_iff theorem

{a b : Nat} : -(a : Int) = -[b+1] ↔ a = b + 1

Full source

@[simp] theorem neg_ofNat_eq_negSucc_iff {a b : Nat} : - (a : Int) = -[b+1] ↔ a = b + 1 := by
  rw [Int.neg_eq_comm]
  rw [Int.neg_negSucc]
  norm_cast
  simp [eq_comm]

Negation of Natural as Integer Equals Negative Successor iff $a = b + 1$

Informal description

For any natural numbers $a$ and $b$, the negation of the natural number $a$ (interpreted as an integer) equals the negative successor $-([b+1])$ if and only if $a$ equals $b + 1$. In symbols: $$ -a = -[b+1] \leftrightarrow a = b + 1 $$

Int.negSucc_eq_neg_ofNat_iff theorem

{a b : Nat} : -[a+1] = -(b : Int) ↔ a + 1 = b

Full source

@[simp] theorem negSucc_eq_neg_ofNat_iff {a b : Nat} : -[a+1]-[a+1] = - (b : Int) ↔ a + 1 = b := by
  rw [eq_comm, neg_ofNat_eq_negSucc_iff, eq_comm]

Negative Successor Equals Negated Natural iff Successor Equality

Informal description

For any natural numbers $a$ and $b$, the negative successor $-([a+1])$ equals the negation of the natural number $b$ (interpreted as an integer) if and only if $a + 1 = b$. In symbols: $$ -[a+1] = -b \leftrightarrow a + 1 = b $$

Int.neg_ofNat_eq_negSucc_add_one_iff theorem

{a b : Nat} : -(a : Int) = -[b+1] + 1 ↔ a = b

Full source

@[simp] theorem neg_ofNat_eq_negSucc_add_one_iff {a b : Nat} : - (a : Int) = -[b+1] + 1 ↔ a = b := by
  cases b with
  | zero => simp; norm_cast
  | succ b =>
    rw [Int.neg_eq_comm, ← Int.negSucc_sub_one, Int.sub_add_cancel, Int.neg_negSucc]
    norm_cast
    simp [eq_comm]

Negation-Negative Successor Addition Equivalence: $-a = -[b+1] + 1 \leftrightarrow a = b$

Informal description

For any natural numbers $a$ and $b$, the negation of $a$ (interpreted as an integer) equals the negative successor $-([b+1])$ plus one if and only if $a = b$. In symbols: $$ -a = -[b+1] + 1 \leftrightarrow a = b $$

Int.negSucc_add_one_eq_neg_ofNat_iff theorem

{a b : Nat} : -[a+1] + 1 = -(b : Int) ↔ a = b

Full source

@[simp] theorem negSucc_add_one_eq_neg_ofNat_iff {a b : Nat} : -[a+1]-[a+1] + 1 = - (b : Int) ↔ a = b := by
  rw [eq_comm, neg_ofNat_eq_negSucc_add_one_iff, eq_comm]

Negative Successor Plus One Equals Negative Natural iff Equality: $-([a+1]) + 1 = -b \leftrightarrow a = b$

Informal description

For any natural numbers $a$ and $b$, the equation $-([a+1]) + 1 = -b$ holds if and only if $a = b$, where $-[a+1]$ denotes the negative successor of $a$ and $-b$ denotes the negation of $b$ interpreted as an integer.

Int.add_left_inj theorem

{i j : Int} (k : Int) : (i + k = j + k) ↔ i = j

Full source

@[simp] protected theorem add_left_inj {i j : Int} (k : Int) : (i + k = j + k) ↔ i = j := by
  apply Iff.intro
  · intro p
    rw [←Int.add_sub_cancel i k, ←Int.add_sub_cancel j k, p]
  · exact congrArg (· + k)

Left Addition Cancellation in Integers: $i + k = j + k \leftrightarrow i = j$

Informal description

For any integers $i$, $j$, and $k$, the equality $i + k = j + k$ holds if and only if $i = j$.

Int.add_right_inj theorem

{i j : Int} (k : Int) : (k + i = k + j) ↔ i = j

Full source

@[simp] protected theorem add_right_inj {i j : Int} (k : Int) : (k + i = k + j) ↔ i = j := by
  simp [Int.add_comm k, Int.add_left_inj]

Right Addition Cancellation in Integers: $k + i = k + j \leftrightarrow i = j$

Informal description

For any integers $i$, $j$, and $k$, the equality $k + i = k + j$ holds if and only if $i = j$.

Int.sub_right_inj theorem

{i j : Int} (k : Int) : (k - i = k - j) ↔ i = j

Full source

@[simp] protected theorem sub_right_inj {i j : Int} (k : Int) : (k - i = k - j) ↔ i = j := by
  simp [Int.sub_eq_add_neg, Int.neg_inj, Int.add_right_inj]

Right Subtraction Cancellation in Integers: $k - i = k - j \leftrightarrow i = j$

Informal description

For any integers $i$, $j$, and $k$, the equality $k - i = k - j$ holds if and only if $i = j$.

Int.sub_left_inj theorem

{i j : Int} (k : Int) : (i - k = j - k) ↔ i = j

Full source

@[simp] protected theorem sub_left_inj {i j : Int} (k : Int) : (i - k = j - k) ↔ i = j := by
  simp [Int.sub_eq_add_neg, Int.add_left_inj]

Left Subtraction Cancellation in Integers: $i - k = j - k \leftrightarrow i = j$

Informal description

For any integers $i$, $j$, and $k$, the equality $i - k = j - k$ holds if and only if $i = j$.

Int.ofNat_mul_negSucc theorem

(m n : Nat) : (m : Int) * -[n+1] = -↑(m * succ n)

Full source

theorem ofNat_mul_negSucc (m n : Nat) : (m : Int) * -[n+1] = -↑(m * succ n) := rfl

Product of Natural Number and Negative Successor in Integers Equals Negative of Product in Naturals

Informal description

For any natural numbers $m$ and $n$, the product of the natural number $m$ (cast as an integer) and the negative successor $- (n + 1)$ in the integers equals the negation of the natural number $m \times (n + 1)$ (cast as an integer), i.e., $$m \times (-[n+1]) = - (m \times (n + 1)).$$

Int.negSucc_mul_ofNat theorem

(m n : Nat) : -[m+1] * n = -↑(succ m * n)

Full source

theorem negSucc_mul_ofNat (m n : Nat) : -[m+1] * n = -↑(succ m * n) := rfl

Product of Negative Successor and Natural Number in Integers Equals Negated Successor Product in Naturals

Informal description

For any natural numbers $m$ and $n$, the product of the negative successor $- (m + 1)$ and $n$ in the integers equals the negation of the successor product $(m + 1) * n$ in the natural numbers, i.e., $$-[m+1] \times n = -((m + 1) \times n).$$

Int.negSucc_mul_negSucc theorem

(m n : Nat) : -[m+1] * -[n+1] = succ m * succ n

Full source

theorem negSucc_mul_negSucc (m n : Nat) : -[m+1] * -[n+1] = succ m * succ n := rfl

Product of Negative Successors in Integers Equals Product of Successors in Naturals

Informal description

For any natural numbers $m$ and $n$, the product of the negative successors $- (m + 1)$ and $- (n + 1)$ in the integers is equal to the product of the successors $(m + 1)$ and $(n + 1)$ in the natural numbers, i.e., $$-[m+1] \times -[n+1] = (m + 1) \times (n + 1).$$

Int.mul_comm theorem

(a b : Int) : a * b = b * a

Full source

protected theorem mul_comm (a b : Int) : a * b = b * a := by
  cases a <;> cases b <;> simp [Nat.mul_comm]

Commutativity of Integer Multiplication: $a \times b = b \times a$

Informal description

For any integers $a$ and $b$, the product $a \times b$ is equal to $b \times a$.

Int.instCommutativeHMul instance

: Std.Commutative (α := Int) (· * ·)

Full source

instance : Std.Commutative (α := Int) (· * ·) := ⟨Int.mul_comm⟩

Commutativity of Integer Multiplication

Informal description

The multiplication operation on the integers is commutative.

Int.ofNat_mul_negOfNat theorem

(m n : Nat) : (m : Nat) * negOfNat n = negOfNat (m * n)

Full source

theorem ofNat_mul_negOfNat (m n : Nat) : (m : Nat) * negOfNat n = negOfNat (m * n) := by
  cases n <;> rfl

Multiplication of Natural Number Cast with Negated Natural Number in Integers

Informal description

For any natural numbers $m$ and $n$, the product of the canonical image of $m$ in the integers and the negation of $n$ (as an integer) equals the negation of the product $m * n$ (as an integer). In symbols: $(m : \mathbb{Z}) \cdot \text{negOfNat}(n) = \text{negOfNat}(m \cdot n)$.

Int.negOfNat_mul_ofNat theorem

(m n : Nat) : negOfNat m * (n : Nat) = negOfNat (m * n)

Full source

theorem negOfNat_mul_ofNat (m n : Nat) : negOfNat m * (n : Nat) = negOfNat (m * n) := by
  rw [Int.mul_comm]; simp [ofNat_mul_negOfNat, Nat.mul_comm]

Multiplication of Negated Natural Number with Natural Number Cast in Integers: $\text{negOfNat}(m) \times n = \text{negOfNat}(m \times n)$

Informal description

For any natural numbers $m$ and $n$, the product of the negation of $m$ (as an integer) and the canonical image of $n$ in the integers equals the negation of the product $m \times n$ (as an integer). In symbols: $$\text{negOfNat}(m) \times n = \text{negOfNat}(m \times n).$$

Int.negSucc_mul_negOfNat theorem

(m n : Nat) : -[m+1] * negOfNat n = ofNat (succ m * n)

Full source

theorem negSucc_mul_negOfNat (m n : Nat) : -[m+1] * negOfNat n = ofNat (succ m * n) := by
  cases n <;> rfl

Product of Negative Successor and Negative Natural Number

Informal description

For any natural numbers $m$ and $n$, the product of the negative successor $- (m + 1)$ and the negative of $n$ (denoted $\text{negOfNat } n$) equals the natural number $(m + 1) * n$ cast to an integer, i.e., $$-[m+1] \times \text{negOfNat } n = (m + 1) \times n.$$

Int.negOfNat_mul_negSucc theorem

(m n : Nat) : negOfNat n * -[m+1] = ofNat (n * succ m)

Full source

theorem negOfNat_mul_negSucc (m n : Nat) : negOfNat n * -[m+1] = ofNat (n * succ m) := by
  rw [Int.mul_comm, negSucc_mul_negOfNat, Nat.mul_comm]

Product of Negative Natural Number and Negative Successor: $\text{negOfNat } n \times -[m+1] = n \times (m + 1)$

Informal description

For any natural numbers $m$ and $n$, the product of the negative of $n$ (denoted $\text{negOfNat } n$) and the negative successor $- (m + 1)$ equals the natural number $n \times (m + 1)$ cast to an integer, i.e., $$\text{negOfNat } n \times -[m+1] = n \times (m + 1).$$

Int.mul_assoc theorem

(a b c : Int) : a * b * c = a * (b * c)

Full source

protected theorem mul_assoc (a b c : Int) : a * b * c = a * (b * c) := by
  cases a <;> cases b <;> cases c <;>
    simp [Nat.mul_assoc, ofNat_mul_negOfNat, negOfNat_mul_ofNat, negSucc_mul_negOfNat, negOfNat_mul_negSucc]

Associativity of Integer Multiplication: $(a \cdot b) \cdot c = a \cdot (b \cdot c)$

Informal description

For any integers $a$, $b$, and $c$, the multiplication operation is associative, i.e., $(a \cdot b) \cdot c = a \cdot (b \cdot c)$.

Int.instAssociativeHMul instance

: Std.Associative (α := Int) (· * ·)

Full source

instance : Std.Associative (α := Int) (· * ·) := ⟨Int.mul_assoc⟩

Associativity of Integer Multiplication

Informal description

The multiplication operation on integers is associative.

Int.mul_left_comm theorem

(a b c : Int) : a * (b * c) = b * (a * c)

Full source

protected theorem mul_left_comm (a b c : Int) : a * (b * c) = b * (a * c) := by
  rw [← Int.mul_assoc, ← Int.mul_assoc, Int.mul_comm a]

Left Commutativity of Integer Multiplication: $a \cdot (b \cdot c) = b \cdot (a \cdot c)$

Informal description

For any integers $a$, $b$, and $c$, the multiplication operation satisfies left commutativity, i.e., $a \cdot (b \cdot c) = b \cdot (a \cdot c)$.

Int.mul_right_comm theorem

(a b c : Int) : a * b * c = a * c * b

Full source

protected theorem mul_right_comm (a b c : Int) : a * b * c = a * c * b := by
  rw [Int.mul_assoc, Int.mul_assoc, Int.mul_comm b]

Right Commutativity of Integer Multiplication: $a \times b \times c = a \times c \times b$

Informal description

For any integers $a$, $b$, and $c$, the product $a \times b \times c$ is equal to $a \times c \times b$.

Int.mul_zero theorem

(a : Int) : a * 0 = 0

Full source

@[simp] protected theorem mul_zero (a : Int) : a * 0 = 0 := by cases a <;> rfl

Multiplication by Zero in Integers: $a \times 0 = 0$

Informal description

For any integer $a$, the product of $a$ and zero is zero, i.e., $a \times 0 = 0$.

Int.zero_mul theorem

(a : Int) : 0 * a = 0

Full source

@[simp] protected theorem zero_mul (a : Int) : 0 * a = 0 := Int.mul_comm .. ▸ a.mul_zero

Zero Multiplication Property in Integers: $0 \times a = 0$

Informal description

For any integer $a$, the product of zero and $a$ is zero, i.e., $0 \times a = 0$.

Int.negOfNat_eq_subNatNat_zero theorem

(n) : negOfNat n = subNatNat 0 n

Full source

theorem negOfNat_eq_subNatNat_zero (n) : negOfNat n = subNatNat 0 n := by cases n <;> rfl

Negation of Natural Number as Subtraction from Zero

Informal description

For any natural number $n$, the negation of $n$ as an integer is equal to the result of subtracting $n$ from $0$ using the `subNatNat` operation, i.e., $\text{negOfNat}(n) = \text{subNatNat}(0, n)$.

Int.ofNat_mul_subNatNat theorem

(m n k : Nat) : m * subNatNat n k = subNatNat (m * n) (m * k)

Full source

theorem ofNat_mul_subNatNat (m n k : Nat) :
    m * subNatNat n k = subNatNat (m * n) (m * k) := by
  cases m with
  | zero => simp [ofNat_zero, Int.zero_mul, Nat.zero_mul, subNatNat_self]
  | succ m => cases n.lt_or_ge k with
    | inl h =>
      have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
      simp [subNatNat_of_lt h, subNatNat_of_lt h']
      rw [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), ← neg_ofNat_succ, Nat.mul_sub_left_distrib,
        ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]; rfl
    | inr h =>
      have h' : succ m * k ≤ succ m * n := Nat.mul_le_mul_left _ h
      simp [subNatNat_of_le h, subNatNat_of_le h', Nat.mul_sub_left_distrib]

Distributivity of Natural Multiplication over Integer Subtraction: $m \cdot \text{subNatNat}(n, k) = \text{subNatNat}(m \cdot n, m \cdot k)$

Informal description

For any natural numbers $m$, $n$, and $k$, the product of $m$ with the integer subtraction $\text{subNatNat}(n, k)$ equals the integer subtraction $\text{subNatNat}(m \cdot n, m \cdot k)$.

Int.negOfNat_add theorem

(m n : Nat) : negOfNat m + negOfNat n = negOfNat (m + n)

Full source

theorem negOfNat_add (m n : Nat) : negOfNat m + negOfNat n = negOfNat (m + n) := by
  cases m <;> cases n <;> simp [Nat.succ_add] <;> rfl

Sum of Negations Equals Negation of Sum for Natural Numbers

Informal description

For any natural numbers $m$ and $n$, the sum of the negation of $m$ and the negation of $n$ is equal to the negation of the sum $m + n$, i.e., $-m + (-n) = -(m + n)$.

Int.negSucc_mul_subNatNat theorem

(m n k : Nat) : -[m+1] * subNatNat n k = subNatNat (succ m * k) (succ m * n)

Full source

theorem negSucc_mul_subNatNat (m n k : Nat) :
    -[m+1] * subNatNat n k = subNatNat (succ m * k) (succ m * n) := by
  cases n.lt_or_ge k with
  | inl h =>
    have h' : succ m * n < succ m * k := Nat.mul_lt_mul_of_pos_left h (Nat.succ_pos m)
    rw [subNatNat_of_lt h, subNatNat_of_le (Nat.le_of_lt h')]
    simp [sub_one_add_one_eq_of_pos (Nat.sub_pos_of_lt h), Nat.mul_sub_left_distrib]
  | inr h => cases Nat.lt_or_ge k n with
    | inl h' =>
      have h₁ : succ m * n > succ m * k := Nat.mul_lt_mul_of_pos_left h' (Nat.succ_pos m)
      rw [subNatNat_of_le h, subNatNat_of_lt h₁, negSucc_mul_ofNat,
        Nat.mul_sub_left_distrib, ← succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁)]; rfl
    | inr h' => rw [Nat.le_antisymm h h', subNatNat_self, subNatNat_self, Int.mul_zero]

Distributivity of Negative Successor Multiplication over Integer Subtraction via $\text{subNatNat}$

Informal description

For any natural numbers $m$, $n$, and $k$, the product of the negative successor $- (m + 1)$ and the integer subtraction operation $\text{subNatNat}(n, k)$ equals the integer subtraction operation applied to the products $(m + 1) \cdot k$ and $(m + 1) \cdot n$, i.e., $$-[m+1] \times \text{subNatNat}(n, k) = \text{subNatNat}((m + 1) \cdot k, (m + 1) \cdot n).$$

Int.mul_add theorem

: ∀ a b c : Int, a * (b + c) = a * b + a * c

Full source

protected theorem mul_add : ∀ a b c : Int, a * (b + c) = a * b + a * c
  | (m:Nat), (n:Nat), (k:Nat) => by simp [Nat.left_distrib]
  | (m:Nat), (n:Nat), -[k+1]  => by
    simp [negOfNat_eq_subNatNat_zero]; rw [← subNatNat_add]; rfl
  | (m:Nat), -[n+1],  (k:Nat) => by
    simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, ← subNatNat_add]; rfl
  | (m:Nat), -[n+1],  -[k+1]  => by simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]
  | -[m+1],  (n:Nat), (k:Nat) => by simp [Nat.mul_comm]; rw [← Nat.right_distrib, Nat.mul_comm]
  | -[m+1],  (n:Nat), -[k+1]  => by
    simp [negOfNat_eq_subNatNat_zero]; rw [Int.add_comm, ← subNatNat_add]; rfl
  | -[m+1],  -[n+1],  (k:Nat) => by simp [negOfNat_eq_subNatNat_zero]; rw [← subNatNat_add]; rfl
  | -[m+1],  -[n+1],  -[k+1]  => by simp [← Nat.left_distrib, Nat.add_left_comm, Nat.add_assoc]

Left Distributivity of Integer Multiplication over Addition: $a \cdot (b + c) = a \cdot b + a \cdot c$

Informal description

For any integers $a$, $b$, and $c$, the product of $a$ with the sum $b + c$ is equal to the sum of the products $a \cdot b$ and $a \cdot c$, i.e., $a \cdot (b + c) = a \cdot b + a \cdot c$.

Int.add_mul theorem

(a b c : Int) : (a + b) * c = a * c + b * c

Full source

protected theorem add_mul (a b c : Int) : (a + b) * c = a * c + b * c := by
  simp [Int.mul_comm, Int.mul_add]

Right Distributivity of Integer Multiplication over Addition: $(a + b) \cdot c = a \cdot c + b \cdot c$

Informal description

For any integers $a$, $b$, and $c$, the product of the sum $a + b$ with $c$ is equal to the sum of the products $a \cdot c$ and $b \cdot c$, i.e., $(a + b) \cdot c = a \cdot c + b \cdot c$.

Int.neg_mul_eq_neg_mul theorem

(a b : Int) : -(a * b) = -a * b

Full source

protected theorem neg_mul_eq_neg_mul (a b : Int) : -(a * b) = -a * b :=
  Int.neg_eq_of_add_eq_zero <| by rw [← Int.add_mul, Int.add_right_neg, Int.zero_mul]

Negation of Product Equals Product of Negation: $-(ab) = (-a)b$

Informal description

For any integers $a$ and $b$, the negation of the product $a \cdot b$ is equal to the product of $-a$ and $b$, i.e., $-(a \cdot b) = (-a) \cdot b$.

Int.neg_mul_eq_mul_neg theorem

(a b : Int) : -(a * b) = a * -b

Full source

protected theorem neg_mul_eq_mul_neg (a b : Int) : -(a * b) = a * -b :=
  Int.neg_eq_of_add_eq_zero <| by rw [← Int.mul_add, Int.add_right_neg, Int.mul_zero]

Negation of Product Equals Product with Negated Factor: $-(a \cdot b) = a \cdot (-b)$

Informal description

For any integers $a$ and $b$, the negation of the product $a \cdot b$ is equal to the product of $a$ with the negation of $b$, i.e., $-(a \cdot b) = a \cdot (-b)$.

Int.neg_mul theorem

(a b : Int) : -a * b = -(a * b)

Full source

protected theorem neg_mul (a b : Int) : -a * b = -(a * b) :=
  (Int.neg_mul_eq_neg_mul a b).symm

Negated Product Identity: $-a \cdot b = -(a \cdot b)$ for Integers

Informal description

For any integers $a$ and $b$, the product of $-a$ and $b$ is equal to the negation of the product $a \cdot b$, i.e., $-a \cdot b = -(a \cdot b)$.

Int.mul_neg theorem

(a b : Int) : a * -b = -(a * b)

Full source

protected theorem mul_neg (a b : Int) : a * -b = -(a * b) :=
  (Int.neg_mul_eq_mul_neg a b).symm

Product with Negated Integer Equals Negation of Product: $a \cdot (-b) = -(a \cdot b)$

Informal description

For any integers $a$ and $b$, the product of $a$ and $-b$ is equal to the negation of the product of $a$ and $b$, i.e., $a \cdot (-b) = -(a \cdot b)$.

Int.neg_mul_neg theorem

(a b : Int) : -a * -b = a * b

Full source

protected theorem neg_mul_neg (a b : Int) : -a * -b = a * b := by simp [Int.neg_mul, Int.mul_neg]

Negation Multiplication Identity: $-a \cdot -b = a \cdot b$ for Integers

Informal description

For any integers $a$ and $b$, the product of $-a$ and $-b$ equals the product of $a$ and $b$, i.e., $-a \cdot -b = a \cdot b$.

Int.neg_mul_comm theorem

(a b : Int) : -a * b = a * -b

Full source

protected theorem neg_mul_comm (a b : Int) : -a * b = a * -b := by simp [Int.neg_mul, Int.mul_neg]

Commutativity of Negation in Integer Multiplication: $-a \cdot b = a \cdot (-b)$

Informal description

For any integers $a$ and $b$, the product of $-a$ and $b$ is equal to the product of $a$ and $-b$, i.e., $-a \cdot b = a \cdot (-b)$.

Int.mul_sub theorem

(a b c : Int) : a * (b - c) = a * b - a * c

Full source

protected theorem mul_sub (a b c : Int) : a * (b - c) = a * b - a * c := by
  simp [Int.sub_eq_add_neg, Int.mul_add, Int.mul_neg]

Left Distributivity of Integer Multiplication over Subtraction: $a \cdot (b - c) = a \cdot b - a \cdot c$

Informal description

For any integers $a$, $b$, and $c$, the product of $a$ with the difference $b - c$ is equal to the difference of the products $a \cdot b$ and $a \cdot c$, i.e., $a \cdot (b - c) = a \cdot b - a \cdot c$.

Int.sub_mul theorem

(a b c : Int) : (a - b) * c = a * c - b * c

Full source

protected theorem sub_mul (a b c : Int) : (a - b) * c = a * c - b * c := by
  simp [Int.sub_eq_add_neg, Int.add_mul, Int.neg_mul]

Right Distributivity of Integer Multiplication over Subtraction: $(a - b) \cdot c = a \cdot c - b \cdot c$

Informal description

For any integers $a$, $b$, and $c$, the product of the difference $a - b$ with $c$ is equal to the difference of the products $a \cdot c$ and $b \cdot c$, i.e., $(a - b) \cdot c = a \cdot c - b \cdot c$.

Int.one_mul theorem

: ∀ a : Int, 1 * a = a

Full source

@[simp] protected theorem one_mul : ∀ a : Int, 1 * a = a
  | ofNat n => show ofNat (1 * n) = ofNat n by rw [Nat.one_mul]
  | -[n+1]  => show -[1 * n +1] = -[n+1] by rw [Nat.one_mul]

Left Multiplicative Identity for Integers: $1 \times a = a$

Informal description

For any integer $a$, the product of $1$ and $a$ equals $a$, i.e., $1 \times a = a$.

Int.mul_one theorem

(a : Int) : a * 1 = a

Full source

@[simp] protected theorem mul_one (a : Int) : a * 1 = a := by rw [Int.mul_comm, Int.one_mul]

Right Multiplicative Identity for Integers: $a \times 1 = a$

Informal description

For any integer $a$, the product of $a$ and $1$ equals $a$, i.e., $a \times 1 = a$.

Int.instLawfulIdentityHMulOfNat instance

: Std.LawfulIdentity (α := Int) (· * ·) 1

Full source

instance : Std.LawfulIdentity (α := Int) (· * ·) 1 where
  left_id := Int.one_mul
  right_id := Int.mul_one

$1$ is the multiplicative identity for integers

Informal description

The integer $1$ is a verified left and right identity element for multiplication on the integers. That is, for any integer $a$, we have $1 \times a = a$ and $a \times 1 = a$.

Int.mul_neg_one theorem

(a : Int) : a * -1 = -a

Full source

@[simp] protected theorem mul_neg_one (a : Int) : a * -1 = -a := by rw [Int.mul_neg, Int.mul_one]

Negation via Multiplication: $a \times (-1) = -a$

Informal description

For any integer $a$, the product of $a$ and $-1$ equals $-a$, i.e., $a \times (-1) = -a$.

Int.neg_one_mul theorem

(a : Int) : -1 * a = -a

Full source

@[simp] protected theorem neg_one_mul (a : Int) : -1 * a = -a := by rw [Int.neg_mul, Int.one_mul]

Negation as Multiplication by Negative One: $-1 \times a = -a$

Informal description

For any integer $a$, the product of $-1$ and $a$ equals $-a$, i.e., $-1 \times a = -a$.

Int.neg_eq_neg_one_mul theorem

: ∀ a : Int, -a = -1 * a

Full source

protected theorem neg_eq_neg_one_mul : ∀ a : Int, -a = -1 * a
  | 0      => rfl
  | succ n => show _ = -[1 * n +1] by rw [Nat.one_mul]; rfl
  | -[n+1] => show _ = ofNat _ by rw [Nat.one_mul]; rfl

Negation as Multiplication by Negative One: $-a = -1 \times a$

Informal description

For any integer $a$, the negation of $a$ is equal to the product of $-1$ and $a$, i.e., $-a = -1 \times a$.

Int.mul_eq_zero theorem

{a b : Int} : a * b = 0 ↔ a = 0 ∨ b = 0

Full source

protected theorem mul_eq_zero {a b : Int} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
  refine ⟨fun h => ?_, fun h => h.elim (by simp [·, Int.zero_mul]) (by simp [·, Int.mul_zero])⟩
  exact match a, b, h with
  | .ofNat 0, _, _ => by simp
  | _, .ofNat 0, _ => by simp
  | .ofNat (a+1), .negSucc b, h => by cases h

Zero Product Property for Integers: $ab = 0 \leftrightarrow a=0 \lor b=0$

Informal description

For any integers $a$ and $b$, the product $a \times b$ equals zero if and only if $a = 0$ or $b = 0$.

Int.mul_ne_zero theorem

{a b : Int} (a0 : a ≠ 0) (b0 : b ≠ 0) : a * b ≠ 0

Full source

protected theorem mul_ne_zero {a b : Int} (a0 : a ≠ 0) (b0 : b ≠ 0) : a * b ≠ 0 :=
  Or.recOr.rec a0 b0 ∘ Int.mul_eq_zero.mp

Nonzero Integers Have Nonzero Product: $a \neq 0 \land b \neq 0 \to a \times b \neq 0$

Informal description

For any integers $a$ and $b$ such that $a \neq 0$ and $b \neq 0$, their product $a \times b$ is not equal to zero.

Int.mul_ne_zero_iff theorem

{a b : Int} : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

Full source

@[simp] protected theorem mul_ne_zero_iff {a b : Int} : a * b ≠ 0a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := by
  rw [ne_eq, Int.mul_eq_zero, not_or, ne_eq]

Nonzero Product Property for Integers: $ab \neq 0 \leftrightarrow a \neq 0 \land b \neq 0$

Informal description

For any integers $a$ and $b$, the product $a \times b$ is nonzero if and only if both $a$ and $b$ are nonzero, i.e., $a \times b \neq 0 \leftrightarrow a \neq 0 \land b \neq 0$.

Int.mul_eq_mul_left_iff theorem

{a b c : Int} (h : c ≠ 0) : c * a = c * b ↔ a = b

Full source

theorem mul_eq_mul_left_iff {a b c : Int} (h : c ≠ 0) : c * a = c * b ↔ a = b :=
  ⟨Int.eq_of_mul_eq_mul_left h, fun w => congrArg (fun x => c * x) w⟩

Left Cancellation Property for Integer Multiplication

Informal description

For any integers $a$, $b$, and $c$ with $c \neq 0$, the equality $c \cdot a = c \cdot b$ holds if and only if $a = b$.

Int.mul_eq_mul_right_iff theorem

{a b c : Int} (h : c ≠ 0) : a * c = b * c ↔ a = b

Full source

theorem mul_eq_mul_right_iff {a b c : Int} (h : c ≠ 0) : a * c = b * c ↔ a = b :=
  ⟨Int.eq_of_mul_eq_mul_right h, fun w => congrArg (fun x => x * c) w⟩

Right Cancellation Property for Integer Multiplication

Informal description

For any integers $a$, $b$, and $c$ with $c \neq 0$, the equality $a \cdot c = b \cdot c$ holds if and only if $a = b$.

Int.natCast_zero theorem

: ((0 : Nat) : Int) = (0 : Int)

Full source

protected theorem natCast_zero : ((0 : Nat) : Int) = (0 : Int) := rfl

Natural Number Zero Maps to Integer Zero

Informal description

The canonical homomorphism from natural numbers to integers maps the natural number $0$ to the integer $0$, i.e., $(0 : \mathbb{N}) = (0 : \mathbb{Z})$.

Int.natCast_one theorem

: ((1 : Nat) : Int) = (1 : Int)

Full source

protected theorem natCast_one : ((1 : Nat) : Int) = (1 : Int) := rfl

Natural Number One Maps to Integer One

Informal description

The canonical homomorphism from natural numbers to integers maps the natural number $1$ to the integer $1$, i.e., $(1 : \mathbb{N}) = (1 : \mathbb{Z})$.

Int.natCast_add theorem

(a b : Nat) : ((a + b : Nat) : Int) = (a : Int) + (b : Int)

Full source

@[simp] protected theorem natCast_add (a b : Nat) : ((a + b : Nat) : Int) = (a : Int) + (b : Int) := by
  -- Note this only works because of local simp attributes in this file,
  -- so it still makes sense to tag the lemmas with `@[simp]`.
  simp

Additivity of Natural Number to Integer Cast: $(a + b : \mathbb{N}) = (a : \mathbb{Z}) + (b : \mathbb{Z})$

Informal description

For any natural numbers $a$ and $b$, the canonical homomorphism from natural numbers to integers maps the sum $a + b$ to the sum of the images of $a$ and $b$, i.e., $(a + b : \mathbb{N}) = (a : \mathbb{Z}) + (b : \mathbb{Z})$.

Int.natCast_succ theorem

(n : Nat) : ((n + 1 : Nat) : Int) = (n : Int) + 1

Full source

protected theorem natCast_succ (n : Nat) : ((n + 1 : Nat) : Int) = (n : Int) + 1 := rfl

Successor Preservation in Natural-to-Integer Homomorphism

Informal description

For any natural number $n$, the canonical homomorphism from natural numbers to integers maps the successor of $n$ (i.e., $n + 1$) to the integer obtained by adding $1$ to the image of $n$ under this homomorphism. In other words, $(n + 1 : \mathbb{N}) = (n : \mathbb{Z}) + 1$.

Int.natCast_mul theorem

(a b : Nat) : ((a * b : Nat) : Int) = (a : Int) * (b : Int)

Full source

@[simp] protected theorem natCast_mul (a b : Nat) : ((a * b : Nat) : Int) = (a : Int) * (b : Int) := by
  simp

Multiplicativity of Natural-to-Integer Cast: $(a \cdot b : \mathbb{N}) = (a : \mathbb{Z}) \cdot (b : \mathbb{Z})$

Informal description

For any natural numbers $a$ and $b$, the canonical homomorphism from natural numbers to integers maps the product $a \cdot b$ to the product of the images of $a$ and $b$, i.e., $(a \cdot b : \mathbb{N}) = (a : \mathbb{Z}) \cdot (b : \mathbb{Z})$.