Basic lemmas about division and modulo for integers

ediv and fdiv

theorem Int.mul_ediv_le_mul_ediv_assoc {a : ℤ} (ha : 0 ≤ a) (b : ℤ) {c : ℤ} (hc : 0 ≤ c) : a * (b / c) ≤ a * b / c

@[deprecated Int.ediv_ediv_of_nonneg (since := "2025-10-06")]

theorem Int.ediv_ediv_eq_ediv_mul {x y z : ℤ} (hy : 0 ≤ y) : x / y / z = x / (y * z)

Alias of Int.ediv_ediv_of_nonneg.

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

emod

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