mathlib documentation

data.nat.dist

def nat.dist  :

Distance (absolute value of difference) between natural numbers.

Equations
theorem nat.dist.def (n m : ) :
n.dist m = n - m + (m - n)

theorem nat.dist_comm (n m : ) :
n.dist m = m.dist n

@[simp]
theorem nat.dist_self (n : ) :
n.dist n = 0

theorem nat.eq_of_dist_eq_zero {n m : } :
n.dist m = 0n = m

theorem nat.dist_eq_zero {n m : } :
n = mn.dist m = 0

theorem nat.dist_eq_sub_of_le {n m : } :
n mn.dist m = m - n

theorem nat.dist_eq_sub_of_le_right {n m : } :
m nn.dist m = n - m

theorem nat.dist_zero_right (n : ) :
n.dist 0 = n

theorem nat.dist_zero_left (n : ) :
0.dist n = n

theorem nat.dist_add_add_right (n k m : ) :
(n + k).dist (m + k) = n.dist m

theorem nat.dist_add_add_left (k n m : ) :
(k + n).dist (k + m) = n.dist m

theorem nat.dist_eq_intro {n m k l : } :
n + m = k + ln.dist k = l.dist m

theorem nat.sub_lt_sub_add_sub (n m k : ) :
n - k n - m + (m - k)

theorem nat.dist.triangle_inequality (n m k : ) :
n.dist k n.dist m + m.dist k

theorem nat.dist_mul_right (n k m : ) :
(n * k).dist (m * k) = (n.dist m) * k

theorem nat.dist_mul_left (k n m : ) :
(k * n).dist (k * m) = k * n.dist m

theorem nat.dist_succ_succ {i j : } :
i.succ.dist j.succ = i.dist j

theorem nat.dist_pos_of_ne {i j : } :
i j0 < i.dist j