chore: rename Int.abs_sign_of_nonzero (#29296)

See discussion at <https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Naming.3A.20ne_zero.20vs.20nonzero/with/537369079>.

Author: Ruben-VandeVelde

Mathlib/Algebra/Order/Group/Unbundled/Int.lean

@@ -123,9 +123,12 @@ theorem abs_ediv_le_abs : ∀ a b : ℤ, |a / b| ≤ |a| :=
       | -[m+1], 0 => Nat.zero_le _
       | -[m+1], n + 1 => Nat.succ_le_succ (Nat.div_le_self _ _))
 
-theorem abs_sign_of_nonzero {z : ℤ} (hz : z ≠ 0) : |z.sign| = 1 := by
+theorem abs_sign_of_ne_zero {z : ℤ} (hz : z ≠ 0) : |z.sign| = 1 := by
   rw [abs_eq_natAbs, natAbs_sign_of_ne_zero hz, Int.ofNat_one]
 
+@[deprecated (since := "2025-09-03")]
+alias abs_sign_of_nonzero := abs_sign_of_ne_zero
+
 protected theorem sign_eq_ediv_abs' (a : ℤ) : sign a = a / |a| :=
   if az : a = 0 then by simp [az]
   else (Int.ediv_eq_of_eq_mul_left (mt abs_eq_zero.1 az) (sign_mul_abs _).symm).symm