Documentation

Mathlib.Data.Int.Associated

Associated elements and the integers #

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

Main results #

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