Lemmas about Int.natAbs

This file contains some results on Int.natAbs, the absolute value of an integer as a natural number.

Main results

• Int.natAbsHom: Int.natAbs bundled as a MonoidWithZeroHom.

def Int.natAbsHom : ℤ →*₀ ℕ

Int.natAbs as a bundled MonoidWithZeroHom.

Equations

• Int.natAbsHom = { toFun := Int.natAbs, map_zero' := Int.natAbs_zero, map_one' := Int.natAbs_one, map_mul' := Int.natAbs_mul }

@[simp]

theorem Int.natAbsHom_apply (m : ℤ) : natAbsHom m = m.natAbs

theorem Int.natAbs_natCast_sub_natCast_of_ge {a b : ℕ} (h : b ≤ a) : (↑a - ↑b).natAbs = a - b

theorem Int.natAbs_natCast_sub_natCast_of_le {a b : ℕ} (h : a ≤ b) : (↑a - ↑b).natAbs = b - a