mathlib

9e00c2bc - feat(ring_theory/int/basic): Induction, nat_abs and units (#6733)

feat(ring_theory/int/basic): Induction, nat_abs and units (#6733) Proves : * Induction on primes (special case for nat) * In `int`, a number and its `nat_abs` are associated * An integer is prime iff its `nat_abs` is prime * Two integers are associated iff they are equal or opposites * Classification of the units in `int` (trivial but handy lemma) Co-authored-by: Ruben-VandeVelde <65514131+Ruben-VandeVelde@users.noreply.github.com>