Mathlib.Data.Int.DivMod

Int.natCast_emod theorem

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

Full source

theorem natCast_emod (m n : Nat) : (↑(m % n) : Int) = m % n := ofNat_emod m n

Canonical Embedding Preserves Remainder Operation

Informal description

For any natural numbers $m$ and $n$, the canonical embedding of the remainder $m \bmod n$ into the integers equals the integer remainder of $m$ divided by $n$, i.e., $\uparrow(m \bmod n) = m \bmod n$ where $\uparrow$ denotes the canonical embedding from natural numbers to integers.

Int.add_emod_right theorem

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

Full source

theorem add_emod_right {a b : Int} : (a + b) % b = a % b := add_emod_self

Modulo Operation Invariance Under Right Addition: $(a + b) \bmod b = a \bmod b$

Informal description

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

Int.add_emod_left theorem

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

Full source

theorem add_emod_left {a b : Int} : (a + b) % a = b % a := add_emod_self_left

Modulo Addition Identity: $(a + b) \bmod a = b \bmod a$

Informal description

For any integers $a$ and $b$, the remainder of $(a + b)$ divided by $a$ is equal to the remainder of $b$ divided by $a$, i.e., $(a + b) \bmod a = b \bmod a$.

Int.mul_ediv_le_mul_ediv_assoc theorem

{a : Int} (ha : 0 ≤ a) (b : Int) {c : Int} (hc : 0 ≤ c) : a * (b / c) ≤ a * b / c

Full source

theorem mul_ediv_le_mul_ediv_assoc {a : Int} (ha : 0 ≤ a) (b : Int) {c : Int} (hc : 0 ≤ c) :
    a * (b / c) ≤ a * b / c := by
  obtain rfl | hlt : c = 0 ∨ 0 < c := by omega
  · simp
  · rw [Int.le_ediv_iff_mul_le hlt, Int.mul_assoc]
    exact Int.mul_le_mul_of_nonneg_left (Int.ediv_mul_le b (Int.ne_of_gt hlt)) ha

Inequality for Integer Division and Multiplication: $a \cdot \lfloor b/c \rfloor \leq \lfloor (a \cdot b)/c \rfloor$

Informal description

For integers $a$ and $c$ with $a \geq 0$ and $c \geq 0$, and for any integer $b$, the following inequality holds: $$a \cdot \left\lfloor \frac{b}{c} \right\rfloor \leq \left\lfloor \frac{a \cdot b}{c} \right\rfloor.$$

Int.ediv_ediv_eq_ediv_mul theorem

(m : Int) {n k : Int} (hn : 0 ≤ n) : m / n / k = m / (n * k)

Full source

theorem ediv_ediv_eq_ediv_mul (m : Int) {n k : Int} (hn : 0 ≤ n) :
    m / n / k = m / (n * k) := by
  have {k : Int} (hk : 0 < k) : m / n / k = m / (n * k) := by
    obtain rfl | hn' : n = 0 ∨ 0 < n := by omega
    · simp
    · apply Int.le_antisymm
      · apply Int.le_ediv_of_mul_le (Int.mul_pos hn' hk)
        calc
          m / n / k * (n * k) = m / n / k * k * n := by ac_rfl
          _ ≤ m / n * n :=
            Int.mul_le_mul_of_nonneg_right (Int.ediv_mul_le (m / n) (Int.ne_of_gt hk)) hn
          _ ≤ m :=
            Int.ediv_mul_le m (Int.ne_of_gt hn')
      · apply Int.le_ediv_of_mul_le hk
        rw [← Int.mul_ediv_mul_of_pos_left m n hk, Int.mul_comm m k, Int.mul_comm (_ / _) k]
        apply Int.mul_ediv_le_mul_ediv_assoc
        · exact Int.le_of_lt hk
        · exact Int.le_of_lt <| Int.mul_pos hn' hk
  · rcases Int.lt_trichotomy 0 k with hk | rfl | hk
    · exact this hk
    · simp
    · rw [← Int.neg_neg (m / n / k), ← Int.ediv_neg, this (Int.neg_pos_of_neg hk), ← Int.ediv_neg,
        Int.mul_neg, Int.neg_neg]

Nested Floor Division Equals Single Floor Division by Product

Informal description

For any integer $m$ and non-negative integers $n$ and $k$, the following equality holds: $$\left\lfloor \frac{\lfloor m/n \rfloor}{k} \right\rfloor = \left\lfloor \frac{m}{n \cdot k} \right\rfloor.$$

Int.fdiv_fdiv_eq_fdiv_mul theorem

(m : Int) {n k : Int} (hn : 0 ≤ n) (hk : 0 ≤ k) : (m.fdiv n).fdiv k = m.fdiv (n * k)

Full source

theorem fdiv_fdiv_eq_fdiv_mul (m : Int) {n k : Int} (hn : 0 ≤ n) (hk : 0 ≤ k) :
    (m.fdiv n).fdiv k = m.fdiv (n * k) := by
  rw [Int.fdiv_eq_ediv_of_nonneg _ hn,
    Int.fdiv_eq_ediv_of_nonneg _ hk,
    Int.fdiv_eq_ediv_of_nonneg _ (Int.mul_nonneg hn hk),
    ediv_ediv_eq_ediv_mul _ hn]

Nested Floor Division Equals Single Floor Division by Product for Non-Negative Divisors

Informal description

For any integer $m$ and non-negative integers $n$ and $k$, the following equality holds: $$\left\lfloor \frac{\lfloor m/n \rfloor}{k} \right\rfloor = \left\lfloor \frac{m}{n \cdot k} \right\rfloor.$$

Int.sub_emod_right theorem

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

Full source

theorem sub_emod_right (a b : Int) : (a - b) % b = a % b :=
  emod_sub_cancel a b

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

Informal description

For any integers $a$ and $b$, the remainder of $(a - b)$ when divided by $b$ is equal to the remainder of $a$ when divided by $b$, i.e., $(a - b) \bmod b = a \bmod b$.

Int.emod_eq_sub_self_emod theorem

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

Full source

theorem emod_eq_sub_self_emod {a b : Int} : a % b = (a - b) % b :=
  (sub_emod_right a b).symm

Modular Equivalence under Subtraction: $a \bmod b = (a - b) \bmod b$

Informal description

For any integers $a$ and $b$, the remainder of $a$ when divided by $b$ is equal to the remainder of $(a - b)$ when divided by $b$, i.e., $a \bmod b = (a - b) \bmod b$.