feat(data/int/basic): Forward direction of is_unit_iff_nat_abs_eq (#…

…14516)

This PR adds the forward direction of `is_unit_iff_nat_abs_eq` as a separate lemma. This is useful since you often have `is_unit n` as a hypothesis, and `is_unit_iff_nat_abs_eq.mp hn` is a bit of a mouthful.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/data/int/basic.lean

@@ -1330,6 +1330,8 @@ 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]
 
+alias is_unit_iff_nat_abs_eq ↔ is_unit.nat_abs_eq _
+
 lemma is_unit_iff_abs_eq {x : ℤ} : is_unit x ↔ abs x = 1 :=
 by rw [is_unit_iff_nat_abs_eq, abs_eq_nat_abs, ←int.coe_nat_one, coe_nat_inj']