feat:(RingTheory/ZMod/CyclicUnits): characterize when (ZMod n)ˣ is cyclic (leanprover-community#26020)

Prove that the group `(ZMod n)ˣ` is cyclic iff one of the following mutually exclusive cases happens:
  - `n = 0` (then `ZMod 0 ≃+* ℤ` and the group of units is cyclic of order 2);
  - `n` = `1`,  `2`  or `4`
  - `n` is a power `p ^ e` of an odd prime number, or twice such a power
  (with `1 ≤ e`).

Some individual cases are proved in passing and are
also directly provided by (n= 0, 1, 2, 4, 8, prime, prime powers).

This is a new PR of leanprover-community#25879 after the migration via fork.
See that PR for the preceding discussion.



Co-authored-by: Junyan Xu <[email protected]>

Author: AntoineChambert-Loir

Mathlib.lean

@@ -5616,6 +5616,7 @@ import Mathlib.RingTheory.WittVector.Truncated
 import Mathlib.RingTheory.WittVector.Verschiebung
 import Mathlib.RingTheory.WittVector.WittPolynomial
 import Mathlib.RingTheory.ZMod
+import Mathlib.RingTheory.ZMod.UnitsCyclic
 import Mathlib.SetTheory.Cardinal.Aleph
 import Mathlib.SetTheory.Cardinal.Arithmetic
 import Mathlib.SetTheory.Cardinal.Basic

Mathlib/Algebra/Group/Subgroup/Ker.lean

@@ -292,6 +292,12 @@ theorem ker_one : (1 : G →* M).ker = ⊤ :=
 theorem ker_id : (MonoidHom.id G).ker = ⊥ :=
   rfl
 
+@[to_additive] theorem ker_eq_top_iff {f : G →* M} : f.ker = ⊤ ↔ f = 1 := by
+  simp_rw [ker, ← top_le_iff, SetLike.le_def, f.ext_iff, Subgroup.mem_top, true_imp_iff]; rfl
+
+@[to_additive] theorem range_eq_bot_iff {f : G →* G'} : f.range = ⊥ ↔ f = 1 := by
+  rw [← le_bot_iff, f.range_eq_map, map_le_iff_le_comap, top_le_iff, comap_bot, ker_eq_top_iff]
+
 @[to_additive]
 theorem ker_eq_bot_iff (f : G →* M) : f.ker = ⊥ ↔ Function.Injective f :=
   ⟨fun h x y hxy => by rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy, fun h =>

Mathlib/Algebra/Group/Units/Hom.lean

@@ -107,6 +107,10 @@ variable {M}
 @[to_additive (attr := simp)]
 theorem coeHom_apply (x : Mˣ) : coeHom M x = ↑x := rfl
 
+@[to_additive]
+theorem coeHom_injective : Function.Injective (coeHom M) :=
+  Units.ext
+
 section DivisionMonoid
 
 variable [DivisionMonoid α]

Mathlib/Algebra/Ring/Parity.lean

@@ -134,11 +134,10 @@ lemma Odd.natCast {R : Type*} [Semiring R] {n : ℕ} (hn : Odd n) : Odd (n : R)
   rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
     ← Nat.cast_two, ← Nat.cast_comm]
 
-lemma Odd.pow (ha : Odd a) : ∀ {n : ℕ}, Odd (a ^ n)
-  | 0 => by
-    rw [pow_zero]
-    exact odd_one
-  | n + 1 => by rw [pow_succ]; exact ha.pow.mul ha
+lemma Odd.pow {n : ℕ} (ha : Odd a) : Odd (a ^ n) := by
+  induction n with
+  | zero => simp [pow_zero]
+  | succ n hrec => rw [pow_succ]; exact hrec.mul ha
 
 lemma Odd.pow_add_pow_eq_zero [IsCancelAdd α] (hn : Odd n) (hab : a + b = 0) :
     a ^ n + b ^ n = 0 := by
@@ -279,6 +278,11 @@ lemma Odd.of_mul_left (h : Odd (m * n)) : Odd m :=
 lemma Odd.of_mul_right (h : Odd (m * n)) : Odd n :=
   (odd_mul.mp h).2
 
+lemma odd_pow_iff {e : ℕ} (he : e ≠ 0) : Odd (n ^ e) ↔ Odd n := by
+  refine ⟨?_, Odd.pow⟩
+  simp only [← Nat.not_even_iff_odd, not_imp_not, even_pow]
+  exact fun h ↦ ⟨h, he⟩
+
 lemma even_div : Even (m / n) ↔ m % (2 * n) / n = 0 := by
   rw [even_iff_two_dvd, dvd_iff_mod_eq_zero, ← Nat.mod_mul_right_div_self, mul_comm]
 

Mathlib/Data/Int/Basic.lean

@@ -101,4 +101,7 @@ lemma eq_of_mod_eq_of_natAbs_sub_lt_natAbs {a b c : ℤ} (h1 : a % b = c)
 lemma natAbs_le_of_dvd_ne_zero (hmn : m ∣ n) (hn : n ≠ 0) : natAbs m ≤ natAbs n :=
   not_lt.mp (mt (eq_zero_of_dvd_of_natAbs_lt_natAbs hmn) hn)
 
+theorem gcd_emod (m n : ℤ) : (m % n).gcd n = m.gcd n := by
+  conv_rhs => rw [← m.emod_add_ediv n, gcd_add_mul_left_left]
+
 end Int

Mathlib/Data/Int/ModEq.lean

@@ -190,6 +190,30 @@ theorem cancel_left_div_gcd (hm : 0 < m) (h : c * a ≡ c * b [ZMOD m]) : a ≡
 theorem of_div (h : a / c ≡ b / c [ZMOD m / c]) (ha : c ∣ a) (ha : c ∣ b) (ha : c ∣ m) :
     a ≡ b [ZMOD m] := by convert h.mul_left' <;> rwa [Int.mul_ediv_cancel']
 
+/-- Cancel left multiplication on both sides of the `≡` and in the modulus.
+
+For cancelling left multiplication in the modulus, see `Int.ModEq.of_mul_left`. -/
+protected theorem mul_left_cancel' (hc : c ≠ 0) :
+    c * a ≡ c * b [ZMOD c * m] → a ≡ b [ZMOD m] := by
+  simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.mul_sub]
+  exact Int.dvd_of_mul_dvd_mul_left hc
+
+protected theorem mul_left_cancel_iff' (hc : c ≠ 0) :
+    c * a ≡ c * b [ZMOD c * m] ↔ a ≡ b [ZMOD m] :=
+  ⟨ModEq.mul_left_cancel' hc, Int.ModEq.mul_left'⟩
+
+/-- Cancel right multiplication on both sides of the `≡` and in the modulus.
+
+For cancelling right multiplication in the modulus, see `Int.ModEq.of_mul_right`. -/
+protected theorem mul_right_cancel' (hc : c ≠ 0) :
+    a * c ≡ b * c [ZMOD m * c] → a ≡ b [ZMOD m] := by
+  simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.sub_mul]
+  exact Int.dvd_of_mul_dvd_mul_right hc
+
+protected theorem mul_right_cancel_iff' (hc : c ≠ 0) :
+    a * c ≡ b * c [ZMOD m * c] ↔ a ≡ b [ZMOD m] :=
+  ⟨ModEq.mul_right_cancel' hc, ModEq.mul_right'⟩
+
 end ModEq
 
 theorem modEq_one : a ≡ b [ZMOD 1] :=

Mathlib/Data/Nat/ModEq.lean

@@ -90,6 +90,9 @@ theorem mod_modEq (a n) : a % n ≡ a [MOD n] :=
 
 namespace ModEq
 
+theorem self_mul_add : ModEq m (m * a + b) b := by
+  simp [Nat.ModEq]
+
 lemma of_dvd (d : m ∣ n) (h : a ≡ b [MOD n]) : a ≡ b [MOD m] :=
   modEq_of_dvd <| Int.ofNat_dvd.mpr d |>.trans h.dvd
 

Mathlib/Data/Nat/Totient.lean

@@ -240,6 +240,11 @@ theorem prime_iff_card_units (p : ℕ) [Fintype (ZMod p)ˣ] :
 theorem totient_two : φ 2 = 1 :=
   (totient_prime prime_two).trans rfl
 
+/-- Euler's totient function is only odd at `1` or `2`. -/
+theorem odd_totient_iff {n : ℕ} :
+    Odd (φ n) ↔ n = 1 ∨ n = 2 := by
+  rcases n with _ | _ | _ | _ <;> simp [Nat.totient_even]
+
 theorem totient_eq_one_iff : ∀ {n : ℕ}, n.totient = 1 ↔ n = 1 ∨ n = 2
   | 0 => by simp
   | 1 => by simp
@@ -252,6 +257,21 @@ theorem totient_eq_one_iff : ∀ {n : ℕ}, n.totient = 1 ↔ n = 1 ∨ n = 2
 theorem dvd_two_of_totient_le_one {a : ℕ} (han : 0 < a) (ha : a.totient ≤ 1) : a ∣ 2 := by
   rcases totient_eq_one_iff.mp <| le_antisymm ha <| totient_pos.2 han with rfl | rfl <;> norm_num
 
+theorem odd_totient_iff_eq_one {n : ℕ} :
+    Odd (φ n) ↔ φ n = 1 := by
+  simp [Nat.odd_totient_iff, Nat.totient_eq_one_iff]
+
+/-- `Nat.totient m` and `Nat.totient n` are coprime iff one of them is 1. -/
+theorem totient_coprime_totient_iff (m n : ℕ) :
+    (φ m).Coprime (φ n) ↔ (m = 1 ∨ m = 2) ∨ (n = 1 ∨ n = 2) := by
+  constructor
+  · rw [← not_imp_not]
+    simp_rw [← odd_totient_iff, not_or, not_odd_iff_even, even_iff_two_dvd]
+    exact fun h ↦ Nat.not_coprime_of_dvd_of_dvd one_lt_two h.1 h.2
+  · simp_rw [← totient_eq_one_iff]
+    rintro (h | h) <;> rw [h]
+    exacts [Nat.coprime_one_left _, Nat.coprime_one_right _]
+
 /-! ### Euler's product formula for the totient function
 
 We prove several different statements of this formula. -/

Mathlib/Data/ZMod/Basic.lean

@@ -36,6 +36,8 @@ open Function ZMod
 
 namespace ZMod
 
+instance : IsDomain (ZMod 0) := inferInstanceAs (IsDomain ℤ)
+
 /-- For non-zero `n : ℕ`, the ring `Fin n` is equivalent to `ZMod n`. -/
 def finEquiv : ∀ (n : ℕ) [NeZero n], Fin n ≃+* ZMod n
   | 0, h => (h.ne _ rfl).elim
@@ -141,6 +143,12 @@ theorem natCast_self (n : ℕ) : (n : ZMod n) = 0 :=
 theorem natCast_self' (n : ℕ) : (n + 1 : ZMod (n + 1)) = 0 := by
   rw [← Nat.cast_add_one, natCast_self (n + 1)]
 
+lemma natCast_pow_eq_zero_of_le (p : ℕ) {m n : ℕ} (h : n ≤ m) :
+    (p ^ m : ZMod (p ^ n)) = 0 := by
+  obtain ⟨q, rfl⟩ := Nat.exists_eq_add_of_le h
+  rw [pow_add, ← Nat.cast_pow]
+  simp
+
 section UniversalProperty
 
 variable {n : ℕ} {R : Type*}
@@ -340,6 +348,9 @@ theorem cast_natCast (h : m ∣ n) (k : ℕ) : (cast (k : ZMod n) : R) = k :=
 theorem cast_intCast (h : m ∣ n) (k : ℤ) : (cast (k : ZMod n) : R) = k :=
   map_intCast (castHom h R) k
 
+theorem castHom_surjective (h : m ∣ n) : Function.Surjective (castHom h (ZMod m)) :=
+  fun a ↦ by obtain ⟨a, rfl⟩ := intCast_surjective a; exact ⟨a, map_intCast ..⟩
+
 end CharDvd
 
 section CharEq
@@ -812,6 +823,10 @@ theorem inv_mul_of_unit {n : ℕ} (a : ZMod n) (h : IsUnit a) : a⁻¹ * a = 1 :
 protected theorem inv_eq_of_mul_eq_one (n : ℕ) (a b : ZMod n) (h : a * b = 1) : a⁻¹ = b :=
   left_inv_eq_right_inv (inv_mul_of_unit a ⟨⟨a, b, h, mul_comm a b ▸ h⟩, rfl⟩) h
 
+@[simp]
+theorem inv_neg_one (n : ℕ) : (-1 : ZMod n)⁻¹ = -1 :=
+  ZMod.inv_eq_of_mul_eq_one n (-1) (-1) (by simp)
+
 lemma inv_mul_eq_one_of_isUnit {n : ℕ} {a : ZMod n} (ha : IsUnit a) (b : ZMod n) :
     a⁻¹ * b = 1 ↔ a = b := by
   -- ideally, this would be `ha.inv_mul_eq_one`, but `ZMod n` is not a `DivisionMonoid`...

Mathlib/Data/ZMod/Coprime.lean

@@ -6,6 +6,7 @@ Authors: Michael Stoll
 import Mathlib.Algebra.EuclideanDomain.Int
 import Mathlib.Data.Nat.Prime.Int
 import Mathlib.Data.ZMod.Basic
+import Mathlib.RingTheory.Int.Basic
 import Mathlib.RingTheory.PrincipalIdealDomain
 
 /-!
@@ -19,6 +20,11 @@ assert_not_exists TwoSidedIdeal
 
 namespace ZMod
 
+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] :