Init.Data.Int.DivMod.Bootstrap

Int.dvd_def theorem

(a b : Int) : (a ∣ b) = Exists (fun c => b = a * c)

Full source

protected theorem dvd_def (a b : Int) : (a ∣ b) = Exists (fun c => b = a * c) := rfl

Definition of Divisibility in Integers

Informal description

For any integers $a$ and $b$, the divisibility relation $a \mid b$ holds if and only if there exists an integer $c$ such that $b = a \cdot c$.

Int.dvd_zero theorem

(n : Int) : n ∣ 0

Full source

@[simp] protected theorem dvd_zero (n : Int) : n ∣ 0 := ⟨0, (Int.mul_zero _).symm⟩

Every Integer Divides Zero: $n \mid 0$

Informal description

For any integer $n$, $n$ divides $0$, i.e., $n \mid 0$.

Int.dvd_refl theorem

(n : Int) : n ∣ n

Full source

@[simp] protected theorem dvd_refl (n : Int) : n ∣ n := ⟨1, (Int.mul_one _).symm⟩

Reflexivity of Divisibility in Integers: $n \mid n$

Informal description

For any integer $n$, $n$ divides itself, i.e., $n \mid n$.

Int.one_dvd theorem

(n : Int) : 1 ∣ n

Full source

@[simp] protected theorem one_dvd (n : Int) : 1 ∣ n := ⟨n, (Int.one_mul n).symm⟩

One Divides All Integers: $1 \mid n$

Informal description

For any integer $n$, the integer $1$ divides $n$, i.e., $1 \mid n$.

Int.dvd_trans theorem

: ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c

Full source

protected theorem dvd_trans : ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c
  | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => Exists.intro (d * e) (by rw [Int.mul_assoc])

Transitivity of Divisibility in Integers: $a \mid b \land b \mid c \implies a \mid c$

Informal description

For any integers $a$, $b$, and $c$, if $a$ divides $b$ and $b$ divides $c$, then $a$ divides $c$.

Int.ofNat_dvd theorem

{m n : Nat} : (↑m : Int) ∣ ↑n ↔ m ∣ n

Full source

@[norm_cast] theorem ofNat_dvd {m n : Nat} : (↑m : Int) ∣ ↑n(↑m : Int) ∣ ↑n ↔ m ∣ n := by
  refine ⟨fun ⟨a, ae⟩ => ?_, fun ⟨k, e⟩ => ⟨k, by rw [e, Int.ofNat_mul]⟩⟩
  match Int.le_total a 0 with
  | .inl h =>
    have := ae.symm ▸ Int.mul_nonpos_of_nonneg_of_nonpos (ofNat_zero_le _) h
    rw [Nat.le_antisymm (ofNat_le.1 this) (Nat.zero_le _)]
    apply Nat.dvd_zero
  | .inr h => match a, eq_ofNat_of_zero_le h with
    | _, ⟨k, rfl⟩ => exact ⟨k, Int.ofNat.inj ae⟩

Preservation of Divisibility under Canonical Embedding: $m \mid n$ in $\mathbb{Z}$ iff $m \mid n$ in $\mathbb{N}$

Informal description

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

Int.zero_dvd theorem

{n : Int} : 0 ∣ n ↔ n = 0

Full source

@[simp] protected theorem zero_dvd {n : Int} : 0 ∣ n0 ∣ n ↔ n = 0 :=
  Iff.intro (fun ⟨k, e⟩ => by rw [e, Int.zero_mul])
            (fun h => h.symm ▸ Int.dvd_refl _)

Zero Divides an Integer if and only if the Integer is Zero

Informal description

For any integer $n$, the integer $0$ divides $n$ if and only if $n$ is equal to $0$.

Int.dvd_mul_right theorem

(a b : Int) : a ∣ a * b

Full source

protected theorem dvd_mul_right (a b : Int) : a ∣ a * b := ⟨_, rfl⟩

Divisibility of Product by First Factor: $a \mid a \times b$

Informal description

For any integers $a$ and $b$, $a$ divides the product $a \times b$.

Int.dvd_mul_left theorem

(a b : Int) : b ∣ a * b

Full source

protected theorem dvd_mul_left (a b : Int) : b ∣ a * b := ⟨_, Int.mul_comm ..⟩

Divisibility of Product by Second Factor: $b \mid a \times b$

Informal description

For any integers $a$ and $b$, the integer $b$ divides the product $a \times b$.

Int.neg_dvd theorem

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

Full source

@[simp] protected theorem neg_dvd {a b : Int} : -a ∣ b-a ∣ b ↔ a ∣ b := by
  constructor <;> exact fun ⟨k, e⟩ =>
    ⟨-k, by simp [e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩

Divisibility by Negated Integer: $-a \mid b \leftrightarrow a \mid b$

Informal description

For any integers $a$ and $b$, the negation $-a$ divides $b$ if and only if $a$ divides $b$, i.e., $-a \mid b \leftrightarrow a \mid b$.

Int.dvd_neg theorem

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

Full source

@[simp] protected theorem dvd_neg {a b : Int} : a ∣ -ba ∣ -b ↔ a ∣ b := by
  constructor <;> exact fun ⟨k, e⟩ =>
    ⟨-k, by simp [← e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩

Divisibility of Negated Integer: $a \mid -b \leftrightarrow a \mid b$

Informal description

For any integers $a$ and $b$, the integer $a$ divides $-b$ if and only if $a$ divides $b$.

Int.natAbs_dvd_natAbs theorem

{a b : Int} : natAbs a ∣ natAbs b ↔ a ∣ b

Full source

@[simp] theorem natAbs_dvd_natAbs {a b : Int} : natAbsnatAbs a ∣ natAbs bnatAbs a ∣ natAbs b ↔ a ∣ b := by
  refine ⟨fun ⟨k, hk⟩ => ?_, fun ⟨k, hk⟩ => ⟨natAbs k, hk.symm ▸ natAbs_mul a k⟩⟩
  rw [← natAbs_ofNat k, ← natAbs_mul, natAbs_eq_natAbs_iff] at hk
  cases hk <;> subst b
  · apply Int.dvd_mul_right
  · rw [← Int.mul_neg]; apply Int.dvd_mul_right

Divisibility of Integers via Absolute Values: $\text{natAbs } a \mid \text{natAbs } b \leftrightarrow a \mid b$

Informal description

For any integers $a$ and $b$, the absolute value of $a$ divides the absolute value of $b$ if and only if $a$ divides $b$.

Int.ofNat_dvd_left theorem

{n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natAbs

Full source

theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z(↑n : Int) ∣ z ↔ n ∣ z.natAbs := by
  rw [← natAbs_dvd_natAbs, natAbs_ofNat]

Divisibility of Integer by Natural Number via Absolute Value: $n \mid z \leftrightarrow n \mid \text{natAbs}(z)$

Informal description

For any natural number $n$ and any integer $z$, the integer $n$ divides $z$ if and only if $n$ divides the absolute value of $z$ (as a natural number), i.e., $n \mid z \leftrightarrow n \mid \text{natAbs}(z)$.

Int.zero_ediv theorem

: ∀ b : Int, 0 / b = 0

Full source

@[simp] theorem zero_ediv : ∀ b : Int, 0 / b = 0
  | ofNat _ => show ofNat _ = _ by simp
  | -[_+1] => show -ofNat _ = _ by simp

Division of Zero by Any Integer is Zero

Informal description

For any integer $b$, the division of $0$ by $b$ equals $0$, i.e., $0 / b = 0$.

Int.ediv_zero theorem

: ∀ a : Int, a / 0 = 0

Full source

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

Integer Division by Zero Yields Zero: $a / 0 = 0$

Informal description

For any integer $a$, the result of integer division of $a$ by zero is zero, i.e., $a / 0 = 0$.

Int.zero_emod theorem

(b : Int) : 0 % b = 0

Full source

@[simp] theorem zero_emod (b : Int) : 0 % b = 0 := rfl

Zero Modulo Any Integer is Zero

Informal description

For any integer $b$, the remainder when $0$ is divided by $b$ is $0$, i.e., $0 \bmod b = 0$.

Int.emod_zero theorem

: ∀ a : Int, a % 0 = a

Full source

@[simp] theorem emod_zero : ∀ a : Int, a % 0 = a
  | ofNat _ => congrArg ofNat <| Nat.mod_zero _
  | -[_+1]  => congrArg negSucc <| Nat.mod_zero _

Modulo by Zero Identity for Integers: $a \% 0 = a$

Informal description

For any integer $a$, the modulo operation with divisor zero satisfies $a \% 0 = a$.

Int.ofNat_emod theorem

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

Full source

@[simp, norm_cast] theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl

Natural Number Modulo Preserved Under Integer Coercion

Informal description

For any natural numbers $m$ and $n$, the canonical image of $m \bmod n$ in the integers equals $m \bmod n$ as computed in the integers, i.e., $\uparrow(m \% n) = m \% n$.

Int.emod_add_ediv theorem

: ∀ a b : Int, a % b + b * (a / b) = a

Full source

theorem emod_add_ediv : ∀ a b : Int, a % b + b * (a / b) = a
  | ofNat _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..
  | ofNat m, -[n+1] => by
    show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
    rw [Int.neg_mul_neg]; exact congrArg ofNat <| Nat.mod_add_div ..
  | -[_+1], 0 => by rw [emod_zero]; rfl
  | -[m+1], succ n => aux m n.succ
  | -[m+1], -[n+1] => aux m n.succ
where
  aux (m n : Nat) : n - (m % n + 1) - (n * (m / n) + n) = -[m+1] := by
    rw [← ofNat_emod, ← ofNat_ediv, ← Int.sub_sub, negSucc_eq, Int.sub_sub n,
      ← Int.neg_neg (_-_), Int.neg_sub, Int.sub_sub_self, Int.add_right_comm]
    exact congrArg (fun x => -(ofNat x + 1)) (Nat.mod_add_div ..)

Division-Remainder Decomposition for Integers: $a \% b + b \cdot (a / b) = a$

Informal description

For any integers $a$ and $b$, the sum of the remainder $a \% b$ and the product $b \cdot (a / b)$ equals $a$, i.e., \[ a \% b + b \cdot (a / b) = a. \]

Int.emod_add_ediv' theorem

(a b : Int) : a % b + a / b * b = a

Full source

/-- Variant of `emod_add_ediv` with the multiplication written the other way around. -/
theorem emod_add_ediv' (a b : Int) : a % b + a / b * b = a := by
  rw [Int.mul_comm]; exact emod_add_ediv ..

Division-Remainder Decomposition for Integers (Multiplicative Commuted Form)

Informal description

For any integers $a$ and $b$, the sum of the remainder $a \% b$ and the product $(a / b) \cdot b$ equals $a$, i.e., \[ a \% b + (a / b) \cdot b = a. \]

Int.ediv_add_emod theorem

(a b : Int) : b * (a / b) + a % b = a

Full source

theorem ediv_add_emod (a b : Int) : b * (a / b) + a % b = a := by
  rw [Int.add_comm]; exact emod_add_ediv ..

Division-Remainder Decomposition for Integers: $b \cdot (a / b) + a \% b = a$

Informal description

For any integers $a$ and $b$, the sum of the product $b \cdot (a / b)$ and the remainder $a \% b$ equals $a$, i.e., \[ b \cdot (a / b) + a \% b = a. \]

Int.ediv_add_emod' theorem

(a b : Int) : a / b * b + a % b = a

Full source

/-- Variant of `ediv_add_emod` with the multiplication written the other way around. -/
theorem ediv_add_emod' (a b : Int) : a / b * b + a % b = a := by
  rw [Int.mul_comm]; exact ediv_add_emod ..

Division-Remainder Decomposition for Integers (Multiplicative Commuted Form)

Informal description

For any integers $a$ and $b$, the sum of the product $(a / b) \cdot b$ and the remainder $a \% b$ equals $a$, i.e., \[ (a / b) \cdot b + a \% b = a. \]

Int.emod_def theorem

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

Full source

theorem emod_def (a b : Int) : a % b = a - b * (a / b) := by
  rw [← Int.add_sub_cancel (a % b), emod_add_ediv]

Remainder Decomposition: $a \% b = a - b \cdot (a / b)$

Informal description

For any integers $a$ and $b$, the remainder $a \% b$ is equal to $a - b \cdot (a / b)$.

Int.ediv_neg theorem

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

Full source

@[simp] theorem ediv_neg : ∀ a b : Int, a / (-b) = -(a / b)
  | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
  | ofNat _, -[_+1] => (Int.neg_neg _).symm
  | ofNat _, succ _ | -[_+1], 0 | -[_+1], succ _ | -[_+1], -[_+1] => rfl

Integer Division Negation Identity: $a / (-b) = -(a / b)$

Informal description

For any integers $a$ and $b$, the integer division of $a$ by $-b$ equals the negation of the integer division of $a$ by $b$, i.e., $a / (-b) = -(a / b)$.

Int.div_def theorem

(a b : Int) : a / b = Int.ediv a b

Full source

protected theorem div_def (a b : Int) : a / b = Int.ediv a b := rfl

Integer Division Equals Euclidean Division

Informal description

For any integers $a$ and $b$, the integer division $a / b$ is equal to the Euclidean division function $\text{ediv}$ applied to $a$ and $b$, i.e., $a / b = \text{ediv}(a, b)$.

Int.add_mul_ediv_right theorem

(a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c = a / c + b

Full source

theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c = a / c + b :=
  suffices ∀ {{a b c : Int}}, 0 < c → (a + b * c).ediv c = a.ediv c + b from
    match Int.lt_trichotomy c 0 with
    | Or.inl hlt => by
      rw [← Int.neg_inj, ← Int.ediv_neg, Int.neg_add, ← Int.ediv_neg, ← Int.neg_mul_neg]
      exact this (Int.neg_pos_of_neg hlt)
    | Or.inr (Or.inl HEq) => absurd HEq H
    | Or.inr (Or.inr hgt) => this hgt
  suffices ∀ {k n : Nat} {a : Int}, (a + n * k.succ).ediv k.succ = a.ediv k.succ + n from
    fun a b c H => match c, eq_succ_of_zero_lt H, b with
      | _, ⟨_, rfl⟩, ofNat _ => this
      | _, ⟨k, rfl⟩, -[n+1] => show (a - n.succ * k.succ).ediv k.succ = a.ediv k.succ - n.succ by
        rw [← Int.add_sub_cancel (ediv ..), ← this, Int.sub_add_cancel]
  fun {k n} => @fun
  | ofNat _ => congrArg ofNat <| Nat.add_mul_div_right _ _ k.succ_pos
  | -[m+1] => by
    show ((n * k.succ : Nat) - m.succ : Int).ediv k.succ = n - (m / k.succ + 1 : Nat)
    by_cases h : m < n * k.succ
    · rw [← Int.ofNat_sub h, ← Int.ofNat_sub ((Nat.div_lt_iff_lt_mul k.succ_pos).2 h)]
      apply congrArg ofNat
      rw [Nat.mul_comm, Nat.mul_sub_div]; rwa [Nat.mul_comm]
    · have h := Nat.not_lt.1 h
      have H {a b : Nat} (h : a ≤ b) : (a : Int) + -((b : Int) + 1) = -[b - a +1] := by
        rw [negSucc_eq, Int.ofNat_sub h]
        simp only [Int.sub_eq_add_neg, Int.neg_add, Int.neg_neg, Int.add_left_comm, Int.add_assoc]
      show ediv (↑(n * succ k) + -((m : Int) + 1)) (succ k) = n + -(↑(m / succ k) + 1 : Int)
      rw [H h, H ((Nat.le_div_iff_mul_le k.succ_pos).2 h)]
      apply congrArg negSucc
      rw [Nat.mul_comm, Nat.sub_mul_div]; rwa [Nat.mul_comm]

Integer Division Identity: $(a + b \cdot c)/c = a/c + b$ for $c \neq 0$

Informal description

For any integers $a$, $b$, and $c$ with $c \neq 0$, the integer division $(a + b \cdot c) / c$ equals $a / c + b$.

Int.add_mul_ediv_left theorem

(a : Int) {b : Int} (c : Int) (H : b ≠ 0) : (a + b * c) / b = a / b + c

Full source

theorem add_mul_ediv_left (a : Int) {b : Int}
    (c : Int) (H : b ≠ 0) : (a + b * c) / b = a / b + c :=
  Int.mul_comm .. ▸ Int.add_mul_ediv_right _ _ H

Integer Division Identity: $(a + b \cdot c)/b = a/b + c$ for $b \neq 0$

Informal description

For any integers $a$, $b$, and $c$ with $b \neq 0$, the integer division $(a + b \cdot c) / b$ equals $a / b + c$.

Int.add_ediv_of_dvd_right theorem

{a b c : Int} (H : c ∣ b) : (a + b) / c = a / c + b / c

Full source

theorem add_ediv_of_dvd_right {a b c : Int} (H : c ∣ b) : (a + b) / c = a / c + b / c :=
  if h : c = 0 then by simp [h] else by
    let ⟨k, hk⟩ := H
    rw [hk, Int.mul_comm c k, Int.add_mul_ediv_right _ _ h,
      ← Int.zero_add (k * c), Int.add_mul_ediv_right _ _ h, Int.zero_ediv, Int.zero_add]

Integer Division Additivity under Divisibility: $(a + b)/c = a/c + b/c$ when $c \mid b$

Informal description

For any integers $a$, $b$, and $c$ such that $c$ divides $b$, the integer division $(a + b)/c$ equals $a/c + b/c$.

Int.add_ediv_of_dvd_left theorem

{a b c : Int} (H : c ∣ a) : (a + b) / c = a / c + b / c

Full source

theorem add_ediv_of_dvd_left {a b c : Int} (H : c ∣ a) : (a + b) / c = a / c + b / c := by
  rw [Int.add_comm, Int.add_ediv_of_dvd_right H, Int.add_comm]

Integer Division Additivity under Divisibility: $(a + b)/c = a/c + b/c$ when $c \mid a$

Informal description

For any integers $a$, $b$, and $c$ such that $c$ divides $a$, the integer division $(a + b)/c$ equals $a/c + b/c$.

Int.mul_ediv_cancel theorem

(a : Int) {b : Int} (H : b ≠ 0) : (a * b) / b = a

Full source

@[simp] theorem mul_ediv_cancel (a : Int) {b : Int} (H : b ≠ 0) : (a * b) / b = a := by
  have := Int.add_mul_ediv_right 0 a H
  rwa [Int.zero_add, Int.zero_ediv, Int.zero_add] at this

Cancellation of Multiplication and Division in Integers: $(a \cdot b)/b = a$ for $b \neq 0$

Informal description

For any integers $a$ and $b$ with $b \neq 0$, the integer division $(a \cdot b) / b$ equals $a$.

Int.mul_ediv_cancel_left theorem

(b : Int) (H : a ≠ 0) : (a * b) / a = b

Full source

@[simp] theorem mul_ediv_cancel_left (b : Int) (H : a ≠ 0) : (a * b) / a = b :=
  Int.mul_comm .. ▸ Int.mul_ediv_cancel _ H

Left Cancellation of Multiplication and Division in Integers: $(a \cdot b)/a = b$ for $a \neq 0$

Informal description

For any integers $a$ and $b$ with $a \neq 0$, the integer division $(a \cdot b) / a$ equals $b$.

Int.ediv_nonneg_iff_of_pos theorem

{a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a

Full source

theorem ediv_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a := by
  rw [Int.div_def]
  match b, h with
  | Int.ofNat (b+1), _ =>
    rcases a with ⟨a⟩ <;> simp [Int.ediv]

Non-negativity of Euclidean Division for Positive Divisors: $0 \leq a / b \leftrightarrow 0 \leq a$ when $b > 0$

Informal description

For any integers $a$ and $b$ with $b > 0$, the Euclidean division $a / b$ is non-negative if and only if $a$ is non-negative, i.e., $0 \leq a / b \leftrightarrow 0 \leq a$.

Int.div_nonneg_iff_of_pos abbrev

Full source

@[deprecated ediv_nonneg_iff_of_pos (since := "2025-02-28")]
abbrev div_nonneg_iff_of_pos := @ediv_nonneg_iff_of_pos

Non-negativity of Integer Division for Positive Divisors: $0 \leq a / b \leftrightarrow 0 \leq a$ when $b > 0$

Informal description

For any integers $a$ and $b$ with $b > 0$, the integer division $a / b$ is non-negative if and only if $a$ is non-negative, i.e., $0 \leq a / b \leftrightarrow 0 \leq a$.

Int.emod_nonneg theorem

: ∀ (a : Int) {b : Int}, b ≠ 0 → 0 ≤ a % b

Full source

theorem emod_nonneg : ∀ (a : Int) {b : Int}, b ≠ 0 → 0 ≤ a % b
  | ofNat _, _, _ => ofNat_zero_le _
  | -[_+1], _, H => Int.sub_nonneg_of_le <| ofNat_le.2 <| Nat.mod_lt _ (natAbs_pos.2 H)

Non-negativity of Integer Remainder: $0 \leq a \% b$ for $b \neq 0$

Informal description

For any integer $a$ and any nonzero integer $b$, the remainder $a \% b$ is non-negative, i.e., $0 \leq a \% b$.

Int.emod_lt_of_pos theorem

(a : Int) {b : Int} (H : 0 < b) : a % b < b

Full source

theorem emod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a % b < b :=
  match a, b, eq_succ_of_zero_lt H with
  | ofNat _, _, ⟨_, rfl⟩ => ofNat_lt.2 (Nat.mod_lt _ (Nat.succ_pos _))
  | -[_+1], _, ⟨_, rfl⟩ => Int.sub_lt_self _ (ofNat_lt.2 <| Nat.succ_pos _)

Remainder is Less Than Divisor for Positive Integers: $a \% b < b$ when $b > 0$

Informal description

For any integer $a$ and positive integer $b > 0$, the remainder of $a$ divided by $b$ satisfies $a \% b < b$.

Int.add_mul_emod_self theorem

{a b c : Int} : (a + b * c) % c = a % c

Full source

@[simp] theorem add_mul_emod_self {a b c : Int} : (a + b * c) % c = a % c :=
  if cz : c = 0 then by
    rw [cz, Int.mul_zero, Int.add_zero]
  else by
    rw [Int.emod_def, Int.emod_def, Int.add_mul_ediv_right _ _ cz, Int.add_comm _ b,
      Int.mul_add, Int.mul_comm, ← Int.sub_sub, Int.add_sub_cancel]

Remainder Invariance under Addition of Multiple: $(a + b \cdot c) \% c = a \% c$

Informal description

For any integers $a$, $b$, and $c$, the remainder of $(a + b \cdot c)$ modulo $c$ is equal to the remainder of $a$ modulo $c$, i.e., $(a + b \cdot c) \% c = a \% c$.

Int.add_mul_emod_self_left theorem

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

Full source

@[simp] theorem add_mul_emod_self_left (a b c : Int) : (a + b * c) % b = a % b := by
  rw [Int.mul_comm, Int.add_mul_emod_self]

Remainder Invariance under Left Addition of Multiple: $(a + b \cdot c) \% b = a \% b$

Informal description

For any integers $a$, $b$, and $c$, the remainder of $(a + b \cdot c)$ modulo $b$ is equal to the remainder of $a$ modulo $b$, i.e., $(a + b \cdot c) \% b = a \% b$.

Int.emod_add_emod theorem

(m n k : Int) : (m % n + k) % n = (m + k) % n

Full source

@[simp] theorem emod_add_emod (m n k : Int) : (m % n + k) % n = (m + k) % n := by
  have := (add_mul_emod_self_left (m % n + k) n (m / n)).symm
  rwa [Int.add_right_comm, emod_add_ediv] at this

Modular Addition Invariance: $(m \% n + k) \% n = (m + k) \% n$

Informal description

For any integers $m$, $n$, and $k$, the remainder of $(m \% n + k)$ modulo $n$ is equal to the remainder of $(m + k)$ modulo $n$, i.e., \[ (m \% n + k) \% n = (m + k) \% n. \]

Int.add_emod_emod theorem

(m n k : Int) : (m + n % k) % k = (m + n) % k

Full source

@[simp] theorem add_emod_emod (m n k : Int) : (m + n % k) % k = (m + n) % k := by
  rw [Int.add_comm, emod_add_emod, Int.add_comm]

Modular Addition Invariance: $(m + n \% k) \% k = (m + n) \% k$

Informal description

For any integers $m$, $n$, and $k$, the remainder of $(m + n \% k)$ modulo $k$ is equal to the remainder of $(m + n)$ modulo $k$, i.e., \[ (m + n \% k) \% k = (m + n) \% k. \]

Int.add_emod theorem

(a b n : Int) : (a + b) % n = (a % n + b % n) % n

Full source

theorem add_emod (a b n : Int) : (a + b) % n = (a % n + b % n) % n := by
  rw [add_emod_emod, emod_add_emod]

Modular Addition of Remainders: $(a + b) \% n = (a \% n + b \% n) \% n$

Informal description

For any integers $a$, $b$, and $n$, the remainder of the sum $a + b$ modulo $n$ is equal to the remainder of the sum of the remainders $a \% n$ and $b \% n$ modulo $n$, i.e., \[ (a + b) \% n = (a \% n + b \% n) \% n. \]

Int.add_emod_eq_add_emod_right theorem

{m n k : Int} (i : Int) (H : m % n = k % n) : (m + i) % n = (k + i) % n

Full source

theorem add_emod_eq_add_emod_right {m n k : Int} (i : Int)
    (H : m % n = k % n) : (m + i) % n = (k + i) % n := by
  rw [← emod_add_emod, ← emod_add_emod k, H]

Modular Equivalence Preserved Under Addition: $(m + i) \bmod n = (k + i) \bmod n$ when $m \equiv k \pmod{n}$

Informal description

For any integers $m$, $n$, $k$, and $i$, if $m \bmod n = k \bmod n$, then $(m + i) \bmod n = (k + i) \bmod n$.

Int.emod_add_cancel_right theorem

{m n k : Int} (i) : (m + i) % n = (k + i) % n ↔ m % n = k % n

Full source

theorem emod_add_cancel_right {m n k : Int} (i) : (m + i) % n = (k + i) % n ↔ m % n = k % n :=
  ⟨fun H => by
    have := add_emod_eq_add_emod_right (-i) H
    rwa [Int.add_neg_cancel_right, Int.add_neg_cancel_right] at this,
  add_emod_eq_add_emod_right _⟩

Modular Equivalence Under Right Addition: $(m + i) \bmod n = (k + i) \bmod n \leftrightarrow m \bmod n = k \bmod n$

Informal description

For any integers $m$, $n$, $k$, and $i$, the equality $(m + i) \bmod n = (k + i) \bmod n$ holds if and only if $m \bmod n = k \bmod n$.

Int.mul_emod_left theorem

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

Full source

@[simp] theorem mul_emod_left (a b : Int) : (a * b) % b = 0 := by
  rw [← Int.zero_add (a * b), Int.add_mul_emod_self, Int.zero_emod]

Product Modulo Divisor Vanishes: $(a \cdot b) \bmod b = 0$

Informal description

For any integers $a$ and $b$, the remainder of the product $a \cdot b$ modulo $b$ is zero, i.e., $(a \cdot b) \bmod b = 0$.

Int.mul_emod_right theorem

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

Full source

@[simp] theorem mul_emod_right (a b : Int) : (a * b) % a = 0 := by
  rw [Int.mul_comm, mul_emod_left]

Product Modulo Multiplicand Vanishes: $(a \cdot b) \bmod a = 0$

Informal description

For any integers $a$ and $b$, the remainder of the product $a \cdot b$ modulo $a$ is zero, i.e., $(a \cdot b) \bmod a = 0$.

Int.mul_emod theorem

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

Full source

theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
  conv => lhs; rw [
    ← emod_add_ediv a n, ← emod_add_ediv' b n, Int.add_mul, Int.mul_add, Int.mul_add,
    Int.mul_assoc, Int.mul_assoc, ← Int.mul_add n _ _, add_mul_emod_self_left,
    ← Int.mul_assoc, add_mul_emod_self]

Modulo of Product Equals Modulo of Factors' Moduli: $(a \cdot b) \% n = ((a \% n) \cdot (b \% n)) \% n$

Informal description

For any integers $a$, $b$, and $n$, the remainder of the product $a \cdot b$ modulo $n$ is equal to the remainder of the product $(a \% n) \cdot (b \% n)$ modulo $n$, i.e., \[ (a \cdot b) \% n = ((a \% n) \cdot (b \% n)) \% n. \]

Int.emod_self theorem

{a : Int} : a % a = 0

Full source

@[simp] theorem emod_self {a : Int} : a % a = 0 := by
  have := mul_emod_left 1 a; rwa [Int.one_mul] at this

Self-Modulo Vanishes: $a \bmod a = 0$

Informal description

For any integer $a$, the remainder of $a$ modulo itself is zero, i.e., $a \bmod a = 0$.

Int.emod_emod_of_dvd theorem

(n : Int) {m k : Int} (h : m ∣ k) : (n % k) % m = n % m

Full source

@[simp] theorem emod_emod_of_dvd (n : Int) {m k : Int}
    (h : m ∣ k) : (n % k) % m = n % m := by
  conv => rhs; rw [← emod_add_ediv n k]
  match k, h with
  | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_emod_self_left]

Nested Remainder Property under Divisibility: $(n \% k) \% m = n \% m$ when $m \mid k$

Informal description

For any integers $n$, $m$, and $k$, if $m$ divides $k$ (denoted $m \mid k$), then the remainder of the remainder of $n$ modulo $k$ modulo $m$ is equal to the remainder of $n$ modulo $m$, i.e., \[ (n \% k) \% m = n \% m. \]

Int.emod_emod theorem

(a b : Int) : (a % b) % b = a % b

Full source

@[simp] theorem emod_emod (a b : Int) : (a % b) % b = a % b := by
  conv => rhs; rw [← emod_add_ediv a b, add_mul_emod_self_left]

Idempotence of Integer Modulo Operation: $(a \% b) \% b = a \% b$

Informal description

For any integers $a$ and $b$, the remainder of $a$ modulo $b$ modulo $b$ is equal to the remainder of $a$ modulo $b$, i.e., $(a \% b) \% b = a \% b$.

Int.sub_emod theorem

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

Full source

theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by
  apply (emod_add_cancel_right b).mp
  rw [Int.sub_add_cancel, ← Int.add_emod_emod, Int.sub_add_cancel, emod_emod]

Modular Subtraction Identity: $(a - b) \bmod n = (a \bmod n - b \bmod n) \bmod n$

Informal description

For any integers $a$, $b$, and $n$, the remainder of $(a - b)$ modulo $n$ is equal to the remainder of $(a \bmod n - b \bmod n)$ modulo $n$, i.e., \[ (a - b) \bmod n = (a \bmod n - b \bmod n) \bmod n. \]

Int.mul_ediv_cancel_of_emod_eq_zero theorem

{a b : Int} (H : a % b = 0) : b * (a / b) = a

Full source

theorem mul_ediv_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : b * (a / b) = a := by
  have := emod_add_ediv a b; rwa [H, Int.zero_add] at this

Integer Division Cancellation: $b \cdot (a / b) = a$ when $a \% b = 0$

Informal description

For any integers $a$ and $b$ such that the remainder of $a$ divided by $b$ is zero (i.e., $a \% b = 0$), the product of $b$ and the integer division of $a$ by $b$ equals $a$, i.e., $b \cdot (a / b) = a$.

Int.ediv_mul_cancel_of_emod_eq_zero theorem

{a b : Int} (H : a % b = 0) : a / b * b = a

Full source

theorem ediv_mul_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : a / b * b = a := by
  rw [Int.mul_comm, mul_ediv_cancel_of_emod_eq_zero H]

Integer Division Cancellation: $(a / b) \cdot b = a$ when $a \bmod b = 0$

Informal description

For any integers $a$ and $b$ such that the remainder of $a$ divided by $b$ is zero (i.e., $a \bmod b = 0$), the integer division of $a$ by $b$ multiplied by $b$ equals $a$, i.e., $(a / b) \cdot b = a$.

Int.dvd_of_emod_eq_zero theorem

{a b : Int} (H : b % a = 0) : a ∣ b

Full source

theorem dvd_of_emod_eq_zero {a b : Int} (H : b % a = 0) : a ∣ b :=
  ⟨b / a, (mul_ediv_cancel_of_emod_eq_zero H).symm⟩

Divisibility from Zero Remainder: $b \% a = 0 \implies a \mid b$

Informal description

For any integers $a$ and $b$, if the remainder of $b$ divided by $a$ is zero (i.e., $b \% a = 0$), then $a$ divides $b$ (denoted $a \mid b$).

Int.emod_eq_zero_of_dvd theorem

: ∀ {a b : Int}, a ∣ b → b % a = 0

Full source

theorem emod_eq_zero_of_dvd : ∀ {a b : Int}, a ∣ b → b % a = 0
  | _, _, ⟨_, rfl⟩ => mul_emod_right ..

Divisibility Implies Zero Remainder: $a \mid b \implies b \bmod a = 0$

Informal description

For any integers $a$ and $b$, if $a$ divides $b$ (i.e., $a \mid b$), then the remainder of $b$ divided by $a$ is zero, i.e., $b \bmod a = 0$.

Int.dvd_iff_emod_eq_zero theorem

{a b : Int} : a ∣ b ↔ b % a = 0

Full source

theorem dvd_iff_emod_eq_zero {a b : Int} : a ∣ ba ∣ b ↔ b % a = 0 :=
  ⟨emod_eq_zero_of_dvd, dvd_of_emod_eq_zero⟩

Divisibility Criterion via Remainder: $a \mid b \leftrightarrow b \bmod a = 0$

Informal description

For any integers $a$ and $b$, $a$ divides $b$ if and only if the remainder of $b$ divided by $a$ is zero, i.e., $a \mid b \leftrightarrow b \bmod a = 0$.

Int.mul_ediv_assoc theorem

(a : Int) : ∀ {b c : Int}, c ∣ b → (a * b) / c = a * (b / c)

Full source

protected theorem mul_ediv_assoc (a : Int) : ∀ {b c : Int}, c ∣ b → (a * b) / c = a * (b / c)
  | _, c, ⟨d, rfl⟩ =>
    if cz : c = 0 then by simp [cz, Int.mul_zero] else by
      rw [Int.mul_left_comm, Int.mul_ediv_cancel_left _ cz, Int.mul_ediv_cancel_left _ cz]

Associativity of Multiplication and Division in Integers: $(a \cdot b)/c = a \cdot (b/c)$ for $c \mid b$

Informal description

For any integer $a$ and integers $b, c$ such that $c$ divides $b$, the integer division $(a \cdot b) / c$ equals $a \cdot (b / c)$.

Int.mul_ediv_assoc' theorem

(b : Int) {a c : Int} (h : c ∣ a) : (a * b) / c = a / c * b

Full source

protected theorem mul_ediv_assoc' (b : Int) {a c : Int}
    (h : c ∣ a) : (a * b) / c = a / c * b := by
  rw [Int.mul_comm, Int.mul_ediv_assoc _ h, Int.mul_comm]

Associativity of Multiplication and Division in Integers (variant): $(a \cdot b)/c = (a/c) \cdot b$ for $c \mid a$

Informal description

For any integer $b$ and integers $a, c$ such that $c$ divides $a$, the integer division $(a \cdot b) / c$ equals $(a / c) \cdot b$.

Int.neg_ediv_of_dvd theorem

: ∀ {a b : Int}, b ∣ a → (-a) / b = -(a / b)

Full source

theorem neg_ediv_of_dvd : ∀ {a b : Int}, b ∣ a → (-a) / b = -(a / b)
  | _, b, ⟨c, rfl⟩ => by
    by_cases bz : b = 0
    · simp [bz]
    · rw [Int.neg_mul_eq_mul_neg, Int.mul_ediv_cancel_left _ bz, Int.mul_ediv_cancel_left _ bz]

Negation of Integer Division Under Divisibility: $(-a)/b = -(a/b)$ when $b \mid a$

Informal description

For any integers $a$ and $b$ such that $b$ divides $a$, the integer division of $-a$ by $b$ equals the negation of the integer division of $a$ by $b$, i.e., $(-a)/b = -(a/b)$.

Int.sub_ediv_of_dvd theorem

(a : Int) {b c : Int} (hcb : c ∣ b) : (a - b) / c = a / c - b / c

Full source

theorem sub_ediv_of_dvd (a : Int) {b c : Int}
    (hcb : c ∣ b) : (a - b) / c = a / c - b / c := by
  rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.add_ediv_of_dvd_right (Int.dvd_neg.2 hcb)]
  congr; exact Int.neg_ediv_of_dvd hcb

Subtraction of Integer Division Under Divisibility: $(a - b)/c = a/c - b/c$ when $c \mid b$

Informal description

For any integers $a$, $b$, and $c$ such that $c$ divides $b$, the integer division $(a - b)/c$ equals $a/c - b/c$.

Int.ediv_mul_cancel theorem

{a b : Int} (H : b ∣ a) : a / b * b = a

Full source

protected theorem ediv_mul_cancel {a b : Int} (H : b ∣ a) : a / b * b = a :=
  ediv_mul_cancel_of_emod_eq_zero (emod_eq_zero_of_dvd H)

Integer Division Cancellation: $(a / b) \cdot b = a$ when $b \mid a$

Informal description

For any integers $a$ and $b$ such that $b$ divides $a$ (i.e., $b \mid a$), the integer division of $a$ by $b$ multiplied by $b$ equals $a$, i.e., $(a / b) \cdot b = a$.

Int.mul_ediv_cancel' theorem

{a b : Int} (H : a ∣ b) : a * (b / a) = b

Full source

protected theorem mul_ediv_cancel' {a b : Int} (H : a ∣ b) : a * (b / a) = b := by
  rw [Int.mul_comm, Int.ediv_mul_cancel H]

Integer Division Cancellation: $a \cdot (b / a) = b$ when $a \mid b$

Informal description

For any integers $a$ and $b$ such that $a$ divides $b$ (i.e., $a \mid b$), the product of $a$ and the integer division of $b$ by $a$ equals $b$, i.e., $a \cdot (b / a) = b$.

Int.emod_pos_of_not_dvd theorem

{a b : Int} (h : ¬a ∣ b) : a = 0 ∨ 0 < b % a

Full source

theorem emod_pos_of_not_dvd {a b : Int} (h : ¬ a ∣ b) : a = 0 ∨ 0 < b % a := by
  rw [dvd_iff_emod_eq_zero] at h
  by_cases w : a = 0
  · simp_all
  · exact Or.inr (Int.lt_iff_le_and_ne.mpr ⟨emod_nonneg b w, Ne.symm h⟩)

Positivity of Remainder for Non-Divisors: $a \nmid b \implies (a = 0 \lor 0 < b \% a)$

Informal description

For any integers $a$ and $b$ such that $a$ does not divide $b$, either $a$ is zero or the remainder $b \% a$ is positive, i.e., $a = 0 \lor 0 < b \% a$.

Int.mul_ediv_self_le theorem

{x k : Int} (h : k ≠ 0) : k * (x / k) ≤ x

Full source

theorem mul_ediv_self_le {x k : Int} (h : k ≠ 0) : k * (x / k) ≤ x :=
  calc k * (x / k)
    _ ≤ k * (x / k) + x % k := Int.le_add_of_nonneg_right (emod_nonneg x h)
    _ = x                   := ediv_add_emod _ _

Integer Division Lower Bound: $k \cdot (x / k) \leq x$ for $k \neq 0$

Informal description

For any integers $x$ and $k$ with $k \neq 0$, the product of $k$ and the integer division of $x$ by $k$ is less than or equal to $x$, i.e., \[ k \cdot (x / k) \leq x. \]

Int.lt_mul_ediv_self_add theorem

{x k : Int} (h : 0 < k) : x < k * (x / k) + k

Full source

theorem lt_mul_ediv_self_add {x k : Int} (h : 0 < k) : x < k * (x / k) + k :=
  calc x
    _ = k * (x / k) + x % k := (ediv_add_emod _ _).symm
    _ < k * (x / k) + k     := Int.add_lt_add_left (emod_lt_of_pos x h) _

Lower bound for integer division: $x < k \cdot \left\lfloor \frac{x}{k} \right\rfloor + k$ when $k > 0$

Informal description

For any integers $x$ and $k$ with $k > 0$, we have the inequality: \[ x < k \cdot \left\lfloor \frac{x}{k} \right\rfloor + k \] where $\left\lfloor \cdot \right\rfloor$ denotes integer division.

Int.bmod_emod theorem

: bmod x m % m = x % m

Full source

@[simp] theorem bmod_emod : bmod x m % m = x % m := by
  dsimp [bmod]
  split <;> simp [Int.sub_emod]

Balanced Modulo Preserves Remainder: $\text{bmod}(x, m) \bmod m = x \bmod m$

Informal description

For any integer $x$ and natural number $m$, the balanced modulo function $\text{bmod}(x, m)$ satisfies $\text{bmod}(x, m) \bmod m = x \bmod m$.

Int.bmod_def theorem

(x : Int) (m : Nat) : bmod x m = if (x % m) < (m + 1) / 2 then x % m else (x % m) - m

Full source

theorem bmod_def (x : Int) (m : Nat) : bmod x m =
  if (x % m) < (m + 1) / 2 then
    x % m
  else
    (x % m) - m :=
  rfl

Definition of Balanced Modulo Function: $\text{bmod}(x, m)$

Informal description

For any integer $x$ and natural number $m$, the balanced modulo function $\text{bmod}(x, m)$ is defined as: \[ \text{bmod}(x, m) = \begin{cases} x \% m & \text{if } x \% m < \frac{m + 1}{2}, \\ x \% m - m & \text{otherwise}, \end{cases} \] where $x \% m$ denotes the standard modulo operation.