Documentation

Mathlib.Data.Int.DivMod

Basic lemmas about division and modulo for integers #

ediv and fdiv #

theorem Int.mul_ediv_le_mul_ediv_assoc {a : Int} (ha : 0 a) (b : Int) {c : Int} (hc : 0 c) :
a * (b / c) a * b / c
@[deprecated Int.ediv_ediv (since := "2025-10-06")]
theorem Int.ediv_ediv_eq_ediv_mul {x y z : Int} (hy : 0 y) :
x / y / z = x / (y * z)

Alias of Int.ediv_ediv.

theorem Int.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)

emod #

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