refactor(Data/ZMod): move coe_int_isUnit_iff_isCoprime to ZMod.Units (#38340)

Move `ZMod.coe_int_isUnit_iff_isCoprime` from `Mathlib.Data.ZMod.Coprime` to `Mathlib.Data.ZMod.Units`, where it more naturally belongs as a statement about units in `ZMod`. The proof is rewritten to only use tools available in `Mathlib.Data.ZMod.Units`, avoiding the dependency on `Mathlib.Algebra.EuclideanDomain.Int`.

This is motivated by the desire to use `coe_int_isUnit_iff_isCoprime` without the overhead of importing `Mathlib.Data.ZMod.Coprime` (see #38339 for a use case).

Author: xroblot

Mathlib/Data/ZMod/Coprime.lean

@@ -5,7 +5,6 @@ Authors: Michael Stoll
 -/
 module
 
-public import Mathlib.Algebra.EuclideanDomain.Int
 public import Mathlib.Data.Nat.Prime.Int
 public import Mathlib.Data.ZMod.Basic
 public import Mathlib.RingTheory.Int.Basic
@@ -24,12 +23,6 @@ assert_not_exists TwoSidedIdeal
 
 namespace ZMod
 
-set_option backward.isDefEq.respectTransparency false in
-theorem coe_int_isUnit_iff_isCoprime (n : ℤ) (m : ℕ) :
-    IsUnit (n : ZMod m) ↔ IsCoprime (m : ℤ) n := by
-  rw [Int.isCoprime_iff_nat_coprime, Nat.coprime_comm, ← isUnit_iff_coprime, Associated.isUnit_iff]
-  simpa only [eq_intCast, Int.cast_natCast] using (Int.associated_natAbs _).map (Int.castRingHom _)
-
 /-- If `p` is a prime and `a` is an integer, then `a : ZMod p` is zero if and only if
 `gcd a p ≠ 1`. -/
 theorem eq_zero_iff_gcd_ne_one {a : ℤ} {p : ℕ} [pp : Fact p.Prime] :

Mathlib/Data/ZMod/Units.lean

@@ -153,4 +153,17 @@ theorem isUnit_inv {m : ℕ} {n : ℤ} (h : IsUnit (n : ZMod m)) :
   rw [isUnit_iff_exists]
   exact ⟨n, inv_mul_of_unit _ h, mul_inv_of_unit _ h⟩
 
+theorem coe_int_isUnit_iff_isCoprime (n : ℤ) (m : ℕ) :
+    IsUnit (n : ZMod m) ↔ IsCoprime (m : ℤ) n := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ⟨unitOfIsCoprime n (isCoprime_comm.mp h), by simp⟩⟩
+  obtain rfl | hm := eq_or_ne m 0
+  · rw [Nat.cast_zero, isCoprime_zero_left]
+    exact_mod_cast h
+  · have : NeZero m := ⟨hm⟩
+    obtain ⟨u, hu⟩ := h
+    have h_coprime := val_coe_unit_coprime u
+    rw [hu, Nat.coprime_iff_gcd_eq_one, ← Int.gcd_natCast_natCast,
+      val_intCast, Int.gcd_emod] at h_coprime
+    rwa [isCoprime_comm, Int.isCoprime_iff_gcd_eq_one]
+
 end ZMod