feat(Data/ZMod/{Basic|Units}): some lemmas on units in ZMod (#10028)

This is the second PR in a sequence that adds auxiliary lemmas from the [EulerProducts](https://github.com/MichaelStollBayreuth/EulerProducts) project to Mathlib.

It adds four lemmas on units in `ZMod n`:
```lean
lemma ZMod.eq_one_of_isUnit_natCast {n : ℕ} (h : IsUnit (n : ZMod 0)) : n = 1

lemma ZMod.isUnit_iff_coprime (m n : ℕ) : IsUnit (m : ZMod n) ↔ m.Coprime n

lemma ZMod.isUnit_prime_of_not_dvd {n p : ℕ} (hp : p.Prime) (h : ¬ p ∣ n) : IsUnit (p : ZMod n)

lemma ZMod.not_isUnit_of_mem_primeFactors {n p : ℕ} (h : p ∈ n.primeFactors) : ¬ IsUnit (p : ZMod n)
```

Mathlib/Data/ZMod/Basic.lean

@@ -36,8 +36,7 @@ open Function
 
 namespace ZMod
 
-instance charZero : CharZero (ZMod 0) :=
-  (by infer_instance : CharZero ℤ)
+instance charZero : CharZero (ZMod 0) := inferInstanceAs (CharZero ℤ)
 
 /-- `val a` is a natural number defined as:
   - for `a : ZMod 0` it is the absolute value of `a`
@@ -89,6 +88,13 @@ theorem val_nat_cast {n : ℕ} (a : ℕ) : (a : ZMod n).val = a % n := by
   · apply Fin.val_nat_cast
 #align zmod.val_nat_cast ZMod.val_nat_cast
 
+theorem val_unit' {n : ZMod 0} : IsUnit n ↔ n.val = 1 := by
+  simp only [val]
+  rw [Int.isUnit_iff, Int.natAbs_eq_iff, Nat.cast_one]
+
+lemma eq_one_of_isUnit_natCast {n : ℕ} (h : IsUnit (n : ZMod 0)) : n = 1 := by
+  rw [← Nat.mod_zero n, ← val_nat_cast, val_unit'.mp h]
+
 theorem val_nat_cast_of_lt {n a : ℕ} (h : a < n) : (a : ZMod n).val = a := by
   rwa [val_nat_cast, Nat.mod_eq_of_lt]
 
@@ -748,6 +754,19 @@ theorem val_coe_unit_coprime {n : ℕ} (u : (ZMod n)ˣ) : Nat.Coprime (u : ZMod
   rw [Units.val_mul, val_mul, nat_cast_mod]
 #align zmod.val_coe_unit_coprime ZMod.val_coe_unit_coprime
 
+lemma isUnit_iff_coprime (m n : ℕ) : IsUnit (m : ZMod n) ↔ m.Coprime n := by
+  refine ⟨fun H ↦ ?_, fun H ↦ (unitOfCoprime m H).isUnit⟩
+  have H' := val_coe_unit_coprime H.unit
+  rw [IsUnit.unit_spec, val_nat_cast m, Nat.coprime_iff_gcd_eq_one] at H'
+  rw [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm, ← H']
+  exact Nat.gcd_rec n m
+
+lemma isUnit_prime_iff_not_dvd {n p : ℕ} (hp : p.Prime) : IsUnit (p : ZMod n) ↔ ¬p ∣ n := by
+  rw [isUnit_iff_coprime, Nat.Prime.coprime_iff_not_dvd hp]
+
+lemma isUnit_prime_of_not_dvd {n p : ℕ} (hp : p.Prime) (h : ¬ p ∣ n) : IsUnit (p : ZMod n) :=
+  (isUnit_prime_iff_not_dvd hp).mpr h
+
 @[simp]
 theorem inv_coe_unit {n : ℕ} (u : (ZMod n)ˣ) : (u : ZMod n)⁻¹ = (u⁻¹ : (ZMod n)ˣ) := by
   have := congr_arg ((↑) : ℕ → ZMod n) (val_coe_unit_coprime u)

Mathlib/Data/ZMod/Units.lean

@@ -62,4 +62,11 @@ theorem unitsMap_surjective [hm : NeZero m] (h : n ∣ m) :
     rw [Nat.add_sub_cancel] at h
     contradiction
 
+-- This needs `Nat.primeFactors`, so cannot go into `Mathlib.Data.ZMod.Basic`.
+open Nat in
+lemma not_isUnit_of_mem_primeFactors {n p : ℕ} (h : p ∈ n.primeFactors) :
+    ¬ IsUnit (p : ZMod n) := by
+  rw [isUnit_iff_coprime]
+  exact (Prime.dvd_iff_not_coprime <| prime_of_mem_primeFactors h).mp <| dvd_of_mem_primeFactors h
+
 end ZMod