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>

Author: adomani

src/algebra/associated.lean

@@ -25,10 +25,6 @@ theorem is_unit_of_dvd_unit {α} [comm_monoid α] {x y : α}
   (xy : x ∣ y) (hu : is_unit y) : is_unit x :=
 is_unit_iff_dvd_one.2 $ dvd_trans xy $ is_unit_iff_dvd_one.1 hu
 
-theorem is_unit_int {n : ℤ} : is_unit n ↔ n.nat_abs = 1 :=
-⟨begin rintro ⟨u, rfl⟩, exact (int.units_eq_one_or u).elim (by simp) (by simp) end,
-  λ h, is_unit_iff_dvd_one.2 ⟨n, by rw [← int.nat_abs_mul_self, h]; refl⟩⟩
-
 lemma is_unit_of_dvd_one [comm_monoid α] : ∀a ∣ 1, is_unit (a:α)
 | a ⟨b, eq⟩ := ⟨units.mk_of_mul_eq_one a b eq.symm, rfl⟩
 

src/algebra/ring/basic.lean

@@ -606,6 +606,9 @@ protected theorem neg_eq_neg_one_mul (u : units α) : -u = -1 * u := by simp
 
 end units
 
+lemma is_unit.neg [ring α] {a : α} : is_unit a → is_unit (-a)
+| ⟨x, hx⟩ := hx ▸ (-x).is_unit
+
 namespace ring_hom
 
 /-- Ring homomorphisms preserve additive inverse. -/

src/data/int/basic.lean

@@ -272,6 +272,9 @@ begin
   { cases h; rw h, rw int.nat_abs_neg, },
 end
 
+lemma nat_abs_eq_iff {a : ℤ} {n : ℕ} : a.nat_abs = n ↔ a = n ∨ a = -n :=
+by rw [←int.nat_abs_eq_nat_abs_iff, int.nat_abs_of_nat]
+
 lemma nat_abs_eq_iff_mul_self_eq {a b : ℤ} : a.nat_abs = b.nat_abs ↔ a * a = b * b :=
 begin
   rw [← abs_eq_iff_mul_self_eq, abs_eq_nat_abs, abs_eq_nat_abs],
@@ -1069,6 +1072,20 @@ units.ext_iff.1 $ nat.units_eq_one ⟨nat_abs u, nat_abs ↑u⁻¹,
 theorem units_eq_one_or (u : units ℤ) : u = 1 ∨ u = -1 :=
 by simpa only [units.ext_iff, units_nat_abs] using nat_abs_eq u
 
+lemma is_unit_eq_one_or {a : ℤ} : is_unit a → a = 1 ∨ a = -1
+| ⟨x, hx⟩ := hx ▸ (units_eq_one_or _).imp (congr_arg coe) (congr_arg coe)
+
+lemma is_unit_iff {a : ℤ} : is_unit a ↔ a = 1 ∨ a = -1 :=
+begin
+  refine ⟨λ h, is_unit_eq_one_or h, λ h, _⟩,
+  rcases h with rfl | rfl,
+  { exact is_unit_one },
+  { exact is_unit_one.neg }
+end
+
+theorem is_unit_iff_nat_abs_eq {n : ℤ} : is_unit n ↔ n.nat_abs = 1 :=
+by simp [nat_abs_eq_iff, is_unit_iff]
+
 lemma units_inv_eq_self (u : units ℤ) : u⁻¹ = u :=
 (units_eq_one_or u).elim (λ h, h.symm ▸ rfl) (λ h, h.symm ▸ rfl)
 

src/ring_theory/int/basic.lean

@@ -149,7 +149,7 @@ lemma exists_unit_of_abs (a : ℤ) : ∃ (u : ℤ) (h : is_unit u), (int.nat_abs
 begin
   cases (nat_abs_eq a) with h,
   { use [1, is_unit_one], rw [← h, one_mul], },
-  { use [-1, is_unit_int.mpr rfl], rw [ ← neg_eq_iff_neg_eq.mp (eq.symm h)],
+  { use [-1, is_unit_one.neg], rw [ ← neg_eq_iff_neg_eq.mp (eq.symm h)],
     simp only [neg_mul_eq_neg_mul_symm, one_mul] }
 end
 
@@ -233,7 +233,7 @@ lemma nat.prime_iff_prime {p : ℕ} : p.prime ↔ _root_.prime (p : ℕ) :=
             by rw [hpb, mul_comm, ← hab, hpb, mul_one]))⟩⟩
 
 lemma nat.prime_iff_prime_int {p : ℕ} : p.prime ↔ _root_.prime (p : ℤ) :=
-⟨λ hp, ⟨int.coe_nat_ne_zero_iff_pos.2 hp.pos, mt is_unit_int.1 hp.ne_one,
+⟨λ hp, ⟨int.coe_nat_ne_zero_iff_pos.2 hp.pos, mt int.is_unit_iff_nat_abs_eq.1 hp.ne_one,
   λ a b h, by rw [← int.dvd_nat_abs, int.coe_nat_dvd, int.nat_abs_mul, hp.dvd_mul] at h;
     rwa [← int.dvd_nat_abs, int.coe_nat_dvd, ← int.dvd_nat_abs, int.coe_nat_dvd]⟩,
   λ hp, nat.prime_iff_prime.2 ⟨int.coe_nat_ne_zero.1 hp.1,