Nearest multiples of an integer

Every integer t lies within |μ| / 2 of a multiple of a nonzero integer μ. It is stated without division, as 2 · |t - c μ| ≤ |μ|. The multiple comes from Lean's balanced division Int.bdiv, whose remainder Int.bmod t m lies in [-(m / 2), (m + 1) / 2) for 0 < m.

Main results

• Int.exists_two_mul_abs_sub_mul_le : ∃ c, 2 * |t - c * μ| ≤ |μ| for μ ≠ 0.

theorem Int.exists_two_mul_abs_sub_mul_le (t : ℤ) {μ : ℤ} (hμ : μ ≠ 0) : ∃ (c : ℤ), 2 * |t - c * μ| ≤ |μ|

Every integer lies within |μ| / 2 of a multiple of a nonzero integer μ.