Associated elements and the integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

int.nat_abs_eq_iff_associated: the absolute value is equal iff integers are associated

theorem int.nat_abs_eq_iff_associated {a b : ℤ} :