mathlib

df8ef379 - feat(data/int/basic algebra/associated): is_unit (a : ℤ) iff a = ±1 (#7058)

feat(data/int/basic algebra/associated): is_unit (a : ℤ) iff a = ±1 (#7058) Besides the title lemma, this PR also moves lemma `is_unit_int` from `algebra/associated` to `data/int/basic`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Ruben-VandeVelde <65514131+Ruben-VandeVelde@users.noreply.github.com>