Associated elements and the integers

This file contains some results on equality up to units in the integers.

Main results

• Int.natAbs_eq_iff_associated: the absolute value is equal iff integers are associated

theorem Int.natAbs_eq_iff_associated {a : ℤ} {b : ℤ} : a.natAbs = b.natAbs ↔ Associated a b